let p be Point of (TOP-REAL 2); :: thesis: for f being circular FinSequence of (TOP-REAL 2) holds Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p)))
let f be circular FinSequence of (TOP-REAL 2); :: thesis: Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p)))

per cases ( not p in rng f or p in rng f ) ;

suppose not p in rng f ; :: thesis: Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p)))

hence Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) by FINSEQ_6:def 2; :: thesis: verum

end;

suppose p in rng f ; :: thesis: Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p)))

then rng (Rotate (f,p)) = rng f by FINSEQ_6:90;
then rng (Y_axis (Rotate (f,p))) = rng (Y_axis f) by Th23;
then ( rng (Incr (Y_axis (Rotate (f,p)))) = rng (Y_axis f) & len (Incr (Y_axis (Rotate (f,p)))) = card (rng (Y_axis f)) ) by SEQ_4:def 21;
hence Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) by SEQ_4:def 21; :: thesis: verum

end;

end;