let p be Point of (TOP-REAL 2); :: thesis: for f being non empty circular FinSequence of (TOP-REAL 2) holds GoB (Rotate (f,p)) = GoB f
let f be non empty circular FinSequence of (TOP-REAL 2); :: thesis: GoB (Rotate (f,p)) = GoB f
( Incr (X_axis f) = Incr (X_axis (Rotate (f,p))) & Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p))) ) by Th26, Th27;
hence GoB (Rotate (f,p)) = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def 2
.= GoB f by GOBOARD2:def 2 ;
:: thesis: verum