let G be Group; :: thesis: for N2 being normal Subgroup of G
for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1)
let N2 be normal Subgroup of G; :: thesis: for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1)
let N1 be strict normal Subgroup of G; :: thesis: (carr N1) * (carr N2) c= (carr N2) * (carr N1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr N1) * (carr N2) or x in (carr N2) * (carr N1) )
assume x in (carr N1) * (carr N2) ; :: thesis: x in (carr N2) * (carr N1)
then consider a, b being Element of G such that
A1: x = a * b and
A2: a in carr N1 and
A3: b in carr N2 ;
a in N1 by A2;
then a |^ b in N1 |^ b by Th58;
then a |^ b in multMagma(# the carrier of N1, the multF of N1 #) by Def13;
then A4: a |^ b in carr N1 ;
b * (a |^ b) = b * ((b ") * (a * b)) by GROUP_1:def 3
.= a * b by Th1 ;
hence x in (carr N2) * (carr N1) by A1, A3, A4; :: thesis: verum