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:16
.= (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:16 ; :: thesis: verum