theorem Th20: :: GOBRD14:20

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