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 Def7
.= ((g . (b " )) * (g . a)) * (g . b) by Def7
.= (((g . b) " ) * (g . a)) * (g . b) by Th41
.= (g . a) |^ (g . b) by GROUP_3:def 2 ; :: thesis: verum