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 . ((((a " ) * (b " )) * a) * b) by GROUP_5:19
.= (g . (((a " ) * (b " )) * a)) * (g . b) by Def7
.= ((g . ((a " ) * (b " ))) * (g . a)) * (g . b) by Def7
.= (((g . (a " )) * (g . (b " ))) * (g . a)) * (g . b) by Def7
.= ((((g . a) " ) * (g . (b " ))) * (g . a)) * (g . b) by Th41
.= ((((g . a) " ) * ((g . b) " )) * (g . a)) * (g . b) by Th41
.= [.(g . a),(g . b).] by GROUP_5:19 ; :: thesis: verum