theorem :: GROUP_23:57
for G1, G2, G3 being Group
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for g being Element of G1 holds (f2 * f1) . g = f2 . (f1 . g)