let G, H be Group; 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; for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).]
let g be Homomorphism of G,H; 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 Def6
.=
((g . ((a ") * (b "))) * (g . a)) * (g . b)
by Def6
.=
(((g . (a ")) * (g . (b "))) * (g . a)) * (g . b)
by Def6
.=
((((g . a) ") * (g . (b "))) * (g . a)) * (g . b)
by Th32
.=
((((g . a) ") * ((g . b) ")) * (g . a)) * (g . b)
by Th32
.=
[.(g . a),(g . b).]
by GROUP_5:16
; verum