theorem :: GOBRD14:22

for f being non constant standard special_circular_sequence holds Cl (LeftComp f) = (LeftComp f) \/ (L~ f)