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

now :: thesis: for a being Element of G st a in [.N1,N3.] "\/" [.N2,N3.] holds
a in [.(N1 "\/" N2),N3.]

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:54;
N2 is Subgroup of N1 "\/" N2 by GROUP_4:60;
then A4: commutators (N2,N3) c= commutators ((N1 "\/" N2),N3) by A3, Th56;
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, Th61;
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, Th61;
A14: len (F1 ^ F2) = (len I1) + (len I2) by A8, A11, FINSEQ_1:22
.= len (I1 ^ I2) by FINSEQ_1:22 ;
rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;
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:60;
then commutators (N1,N3) c= commutators ((N1 "\/" N2),N3) by A3, Th56;
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;
Product ((F1 ^ F2) |^ (I1 ^ I2)) = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A8, A11, GROUP_4:19
.= a by A5, A10, A13, GROUP_4:5 ;
hence a in [.(N1 "\/" N2),N3.] by A16, A14, Th61; :: thesis: verum

end;

then A17: [.N1,N3.] "\/" [.N2,N3.] is Subgroup of [.(N1 "\/" N2),N3.] by GROUP_2:58;
commutators ((N1 "\/" N2),N3) c= [.N1,N3.] * [.N2,N3.]

proof

let x be object ; :: 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 Th52;
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, Th65;
then [.c,b.] |^ d in [.N1,N3.] |^ d by GROUP_3:58;
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, Th25, Th65;
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:32;
then [.(N1 "\/" N2),N3.] is Subgroup of [.N1,N3.] "\/" [.N2,N3.] by GROUP_4:50;
hence [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.] by A17, GROUP_2:55; :: thesis: verum