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

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