{T P R : E →ₗ[ℂ] E} {z : ℂ} {s : ℝ} (hcomm : ∀ x, T (P x) = P (T x)) (hR1 : ∀ x, R (T x - z • x) = x) (hR2 : ∀ x, T (R x) - z • R x = x) {x : E} (hx : x ∈ paritySector P s) : R x ∈ paritySector P s

Initializing...

{T P R : E →ₗ[ℂ] E} {z : ℂ} {s : ℝ} (hcomm : ∀ x, T (P x) = P (T x)) (hR1 : ∀ x, R (T x - z • x) = x) (hR2 : ∀ x, T (R x) - z • R x = x) {x : E} (hx : x ∈ paritySector P s) : R x ∈ paritySector P s · Prove2Me