theorem Th20: :: GOBRD14:20

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