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