let G, H be Group; :: thesis: for a1, a2, a3 being Element of G
for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
let a1, a2, a3 be Element of G; :: thesis: for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
let g be Homomorphism of G,H; :: thesis: g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
thus g . [.a1,a2,a3.] = g . [.[.a1,a2.],a3.] by GROUP_5:def 3
.= [.(g . [.a1,a2.]),(g . a3).] by Th34
.= [.[.(g . a1),(g . a2).],(g . a3).] by Th34
.= [.(g . a1),(g . a2),(g . a3).] by GROUP_5:def 3 ; :: thesis: verum