let p be Point of (TOP-REAL 2); :: thesis: for f being V8() standard special_circular_sequence holds RightComp (Rotate f,p) = RightComp f
let f be V8() standard special_circular_sequence; :: thesis: RightComp (Rotate f,p) = RightComp f
A1: RightComp (Rotate f,p) = LeftComp (Rev (Rotate f,p)) by GOBOARD9:26
.= LeftComp (Rotate (Rev f),p) by Th29 ;
RightComp f = LeftComp (Rev f) by GOBOARD9:26;
hence RightComp (Rotate f,p) = RightComp f by A1, Th36; :: thesis: verum