let p be Point of ; :: thesis: for f being circular FinSequence of holds Incr (Y_axis f) = Incr (Y_axis (Rotate f,p))
let f be circular FinSequence of ; :: 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:96;
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 GOBOARD2:def 2;
hence Incr (Y_axis f) = Incr (Y_axis (Rotate f,p)) by GOBOARD2:def 2; :: thesis: verum

end;

end;