let G1, G2, G3 be Group; :: thesis: 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)
let f1 be Homomorphism of G1,G2; :: thesis: for f2 being Homomorphism of G2,G3
for g being Element of G1 holds (f2 * f1) . g = f2 . (f1 . g)
let f2 be Homomorphism of G2,G3; :: thesis: for g being Element of G1 holds (f2 * f1) . g = f2 . (f1 . g)
let g be Element of G1; :: thesis: (f2 * f1) . g = f2 . (f1 . g)
dom f1 = the carrier of G1 by FUNCT_2:def 1;
hence (f2 * f1) . g = f2 . (f1 . g) by FUNCT_1:13; :: thesis: verum