for f being non constant standard special_circular_sequence holds (Cl (RightComp f)) ` = LeftComp f