let O be set ; :: thesis: for G, H, I being GroupWithOperators of O

for h being Homomorphism of G,H

for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let G, H, I be GroupWithOperators of O; :: thesis: for h being Homomorphism of G,H

for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let h be Homomorphism of G,H; :: thesis: for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let h1 be Homomorphism of H,I; :: thesis: h1 * h is Homomorphism of G,I

reconsider f = h1 * h as Function of G,I ;

for h being Homomorphism of G,H

for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let G, H, I be GroupWithOperators of O; :: thesis: for h being Homomorphism of G,H

for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let h be Homomorphism of G,H; :: thesis: for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

let h1 be Homomorphism of H,I; :: thesis: h1 * h is Homomorphism of G,I

reconsider f = h1 * h as Function of G,I ;

now :: thesis: for o being Element of O

for g being Element of G holds f . ((G ^ o) . g) = (I ^ o) . (f . g)

hence
h1 * h is Homomorphism of G,I
by Def18; :: thesis: verumfor g being Element of G holds f . ((G ^ o) . g) = (I ^ o) . (f . g)

let o be Element of O; :: thesis: for g being Element of G holds f . ((G ^ o) . g) = (I ^ o) . (f . g)

let g be Element of G; :: thesis: f . ((G ^ o) . g) = (I ^ o) . (f . g)

thus f . ((G ^ o) . g) = h1 . (h . ((G ^ o) . g)) by FUNCT_2:15

.= h1 . ((H ^ o) . (h . g)) by Def18

.= (I ^ o) . (h1 . (h . g)) by Def18

.= (I ^ o) . (f . g) by FUNCT_2:15 ; :: thesis: verum

end;let g be Element of G; :: thesis: f . ((G ^ o) . g) = (I ^ o) . (f . g)

thus f . ((G ^ o) . g) = h1 . (h . ((G ^ o) . g)) by FUNCT_2:15

.= h1 . ((H ^ o) . (h . g)) by Def18

.= (I ^ o) . (h1 . (h . g)) by Def18

.= (I ^ o) . (f . g) by FUNCT_2:15 ; :: thesis: verum