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 set ; :: 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, STRUCT_0:def 5;
then a |^ b in N1 |^ b by Th70;
then a |^ b in multMagma(# the carrier of N1,the multF of N1 #) by Def13;
then A4: a |^ b in carr N1 by STRUCT_0:def 5;
b * (a |^ b) = b * ((b " ) * (a * b)) by GROUP_1:def 4
.= a * b by Th1 ;
hence x in (carr N2) * (carr N1) by A1, A3, A4; :: thesis: verum