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