let O be set ; :: thesis: for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds union (Cosets N) = the carrier of G
let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds union (Cosets N) = the carrier of G
let N be normal StableSubgroup of G; :: thesis: union (Cosets N) = the carrier of G
reconsider H = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by Lm7;

now

consider h being Element of H;
let x be set ; :: thesis: ( x in the carrier of G implies x in union (Cosets H) )
reconsider g = h as Element of G by GROUP_2:51;
assume x in the carrier of G ; :: thesis: x in union (Cosets H)
then reconsider a = x as Element of G ;
A1: a = a * (1_ G) by GROUP_1:def 5
.= a * ((g " ) * g) by GROUP_1:def 6
.= (a * (g " )) * g by GROUP_1:def 4 ;
A2: (a * (g " )) * H in Cosets H by GROUP_2:def 15;
h in H by STRUCT_0:def 5;
then a in (a * (g " )) * H by A1, GROUP_2:125;
hence x in union (Cosets H) by A2, TARSKI:def 4; :: thesis: verum

end;

then A3: the carrier of G c= union (Cosets H) by TARSKI:def 3;
Cosets N = Cosets H by Def14;
hence union (Cosets N) = the carrier of G by A3, XBOOLE_0:def 10; :: thesis: verum