theorem :: GOBRD12:10

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