let p be Point of (TOP-REAL 2); :: thesis: for f being circular FinSequence of (TOP-REAL 2) holds Incr (X_axis f) = Incr (X_axis (Rotate (f,p)))
let f be circular FinSequence of (TOP-REAL 2); :: thesis: Incr (X_axis f) = Incr (X_axis (Rotate (f,p)))
per cases ( not p in rng f or p in rng f ) ;
suppose not p in rng f ; :: thesis: Incr (X_axis f) = Incr (X_axis (Rotate (f,p)))
hence Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) by FINSEQ_6:def 2; :: thesis: verum
end;
suppose p in rng f ; :: thesis: Incr (X_axis f) = Incr (X_axis (Rotate (f,p)))
then rng (Rotate (f,p)) = rng f by FINSEQ_6:90;
then rng (X_axis (Rotate (f,p))) = rng (X_axis f) by Th21;
then ( rng (Incr (X_axis (Rotate (f,p)))) = rng (X_axis f) & len (Incr (X_axis (Rotate (f,p)))) = card (rng (X_axis f)) ) by SEQ_4:def 21;
hence Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) by SEQ_4:def 21; :: thesis: verum
end;
end;