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 by Th77;
A2: [.N2,N3.] is normal Subgroup of G by Th77;

now

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

end;

then A17: [.N1,N3.] "\/" [.N2,N3.] is Subgroup of [.(N1 "\/" N2),N3.] by GROUP_2:67;
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
A18: x = [.a,b.] and
A19: a in N1 "\/" N2 and
A20: b in N3 by Th58;
consider c, d being Element of G such that
A21: a = c * d and
A22: c in N1 and
A23: d in N2 by A19, Th7;
[.c,b.] in [.N1,N3.] by A20, A22, Th74;
then [.c,b.] |^ d in [.N1,N3.] |^ d by GROUP_3:70;
then A24: [.c,b.] |^ d in [.N1,N3.] by A1, GROUP_3:def 13;
( x = ([.c,b.] |^ d) * [.d,b.] & [.d,b.] in [.N2,N3.] ) by A18, A20, A21, A23, Th28, Th74;
hence x in [.N1,N3.] * [.N2,N3.] by A24, Th4; :: thesis: verum

end;

then gr (commutators (N1 "\/" N2),N3) is Subgroup of gr ([.N1,N3.] * [.N2,N3.]) by GROUP_4:41;
then [.(N1 "\/" N2),N3.] is Subgroup of [.N1,N3.] "\/" [.N2,N3.] by GROUP_4:68;
hence [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.] by A17, GROUP_2:64; :: thesis: verum