theorem Th19: :: GOBRD14:19

for f being V8() standard special_circular_sequence holds L~ f = (Cl (RightComp f)) \ (RightComp f)