let G be Group; :: thesis: for N1, N2, N3 being strict normal Subgroup of G holds [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]
let N1, N2, N3 be strict normal Subgroup of G; :: thesis: [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]
A1: ( [.N1,N3.] is normal Subgroup of G & [.N2,N3.] is normal Subgroup of G ) by Th77;
commutators (N1 "\/" N2),N3 c= [.N1,N3.] * [.N2,N3.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (N1 "\/" N2),N3 or x in [.N1,N3.] * [.N2,N3.] )
assume x in commutators (N1 "\/" N2),N3 ; :: thesis: x in [.N1,N3.] * [.N2,N3.]
then consider a, b being Element of G such that
A2: x = [.a,b.] and
A3: a in N1 "\/" N2 and
A4: b in N3 by Th58;
consider c, d being Element of G such that
A5: a = c * d and
A6: c in N1 and
A7: d in N2 by A3, Th7;
A8: x = ([.c,b.] |^ d) * [.d,b.] by A2, A5, Th28;
[.c,b.] in [.N1,N3.] by A4, A6, Th74;
then [.c,b.] |^ d in [.N1,N3.] |^ d by GROUP_3:70;
then ( [.c,b.] |^ d in [.N1,N3.] & [.d,b.] in [.N2,N3.] ) by A1, A4, A7, Th74, GROUP_3:def 13;
hence x in [.N1,N3.] * [.N2,N3.] by A8, Th4; :: thesis: verum

end;

then gr (commutators (N1 "\/" N2),N3) is Subgroup of gr ([.N1,N3.] * [.N2,N3.]) by GROUP_4:41;
then A9: [.(N1 "\/" N2),N3.] is Subgroup of [.N1,N3.] "\/" [.N2,N3.] by GROUP_4:68;

now

let a be Element of G; :: thesis: ( a in [.N1,N3.] "\/" [.N2,N3.] implies a in [.(N1 "\/" N2),N3.] )
assume a in [.N1,N3.] "\/" [.N2,N3.] ; :: thesis: a in [.(N1 "\/" N2),N3.]
then consider b, c being Element of G such that
A10: a = b * c and
A11: b in [.N1,N3.] and
A12: c in [.N2,N3.] by A1, Th7;
consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A13: len F1 = len I1 and
A14: rng F1 c= commutators N1,N3 and
A15: b = Product (F1 |^ I1) by A11, Th69;
consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT such that
A16: len F2 = len I2 and
A17: rng F2 c= commutators N2,N3 and
A18: c = Product (F2 |^ I2) by A12, Th69;
A19: Product ((F1 ^ F2) |^ (I1 ^ I2)) = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A13, A16, GROUP_4:25
.= a by A10, A15, A18, GROUP_4:8 ;
rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:44;
then A20: rng (F1 ^ F2) c= (commutators N1,N3) \/ (commutators N2,N3) by A14, A17, XBOOLE_1:13;
( N1 is Subgroup of N1 "\/" N2 & N2 is Subgroup of N1 "\/" N2 & N3 is Subgroup of N3 ) by GROUP_2:63, GROUP_4:78;
then ( commutators N1,N3 c= commutators (N1 "\/" N2),N3 & commutators N2,N3 c= commutators (N1 "\/" N2),N3 ) by Th62;
then (commutators N1,N3) \/ (commutators N2,N3) c= commutators (N1 "\/" N2),N3 by XBOOLE_1:8;
then A21: rng (F1 ^ F2) c= commutators (N1 "\/" N2),N3 by A20, XBOOLE_1:1;
len (F1 ^ F2) = (len I1) + (len I2) by A13, A16, FINSEQ_1:35
.= len (I1 ^ I2) by FINSEQ_1:35 ;
hence a in [.(N1 "\/" N2),N3.] by A19, A21, Th69; :: thesis: verum

end;

then [.N1,N3.] "\/" [.N2,N3.] is Subgroup of [.(N1 "\/" N2),N3.] by GROUP_2:67;
hence [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.] by A9, GROUP_2:64; :: thesis: verum