theorem Th70: :: MONOID_0:70

for X being set
for F being non empty SubStr of GPFuncs X
for f, g being Element of F holds f [*] g = g (*) f