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 Th21; :: thesis: verum