theorem :: GROUP_5:71

for G being Group
for N1, N2, N3 being strict normal Subgroup of G holds [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]