let f be non constant standard special_circular_sequence; :: thesis: RightComp (Rev f) = LeftComp f
Rev (Rev f) = f ;
hence RightComp (Rev f) = LeftComp f by Th23; :: thesis: verum