let G be addGroup; :: 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 A4: a * b in carr N1 by Def13;
b + (a * b) = b + ((- b) + (a + b)) by RLVECT_1:def 3
.= a + b by Th1 ;
hence x in (carr N2) + (carr N1) by A1, A3, A4; :: thesis: verum