let G, H be Group; :: thesis: for a, b being Element of G
for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b)
let a, b be Element of G; :: thesis: for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b)
let g be Homomorphism of G,H; :: thesis: g . (a |^ b) = (g . a) |^ (g . b)
thus g . (a |^ b) = g . (((b ") * a) * b) by GROUP_3:def 2
.= (g . ((b ") * a)) * (g . b) by Def6
.= ((g . (b ")) * (g . a)) * (g . b) by Def6
.= (((g . b) ") * (g . a)) * (g . b) by Th32
.= (g . a) |^ (g . b) by GROUP_3:def 2 ; :: thesis: verum