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 3
.= GoB f by GOBOARD2:def 3 ;
:: thesis: verum