let G, H, I be Group; :: thesis: for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is multiplicative
let h be Homomorphism of G,H; :: thesis: for h1 being Homomorphism of H,I holds h1 * h is multiplicative
let h1 be Homomorphism of H,I; :: thesis: h1 * h is multiplicative
set f = h1 * h;
let a be Element of G; :: according to GROUP_6:def 6 :: thesis: for b being Element of G holds (h1 * h) . (a * b) = ((h1 * h) . a) * ((h1 * h) . b)
let b be Element of G; :: thesis: (h1 * h) . (a * b) = ((h1 * h) . a) * ((h1 * h) . b)
thus (h1 * h) . (a * b) = h1 . (h . (a * b)) by FUNCT_2:15
.= h1 . ((h . a) * (h . b)) by Def6
.= (h1 . (h . a)) * (h1 . (h . b)) by Def6
.= ((h1 * h) . a) * (h1 . (h . b)) by FUNCT_2:15
.= ((h1 * h) . a) * ((h1 * h) . b) by FUNCT_2:15 ; :: thesis: verum