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 f = LeftComp (Rev f) by GOBOARD9:23;
RightComp (Rotate (f,p)) = LeftComp (Rev (Rotate (f,p))) by GOBOARD9:23
.= LeftComp (Rotate ((Rev f),p)) by Th29 ;
hence RightComp (Rotate (f,p)) = RightComp f by A1, Th36; :: thesis: verum