theorem Th31: :: GOBRD14:31

for g being constant standard clockwise_oriented special_circular_sequence holds RightComp g c= RightComp (SpStSeq (L~ g))