theorem Th72: :: GROUP_22:67

for G1, G2, G3 being Group
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for A being Subgroup of G1 holds multMagma(# the carrier of (f2 .: (f1 .: A)), the multF of (f2 .: (f1 .: A)) #) = multMagma(# the carrier of ((f2 * f1) .: A), the multF of ((f2 * f1) .: A) #)