let X be set ; :: thesis: for F being non empty SubStr of GPFuncs X
for f, g being Element of F holds f [*] g = g (*) f
let F be non empty SubStr of GPFuncs X; :: thesis: for f, g being Element of F holds f [*] g = g (*) f
let f, g be Element of F; :: thesis: f [*] g = g (*) f
H₁(F) c= H₁( GPFuncs X) by Th23;
then reconsider f9 = f, g9 = g as Element of (GPFuncs X) ;
f [*] g = f9 [*] g9 by Th25;
hence f [*] g = g (*) f by Def37; :: thesis: verum