let x be set ; :: thesis: for G being Group
for N1, N2 being strict normal Subgroup of G holds
( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )
let G be Group; :: thesis: for N1, N2 being strict normal Subgroup of G holds
( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )
let N1, N2 be strict normal Subgroup of G; :: thesis: ( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )
N1 * N2 = N2 * N1 by GROUP_3:125;
hence ( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) ) by Th5; :: thesis: verum