let O be set ; :: thesis: for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds union () = the carrier of G

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds union () = the carrier of G
let N be normal StableSubgroup of G; :: thesis: union () = the carrier of G
reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
now :: thesis: for x being object st x in the carrier of G holds
x in union ()
set h = the Element of H;
let x be object ; :: thesis: ( x in the carrier of G implies x in union () )
reconsider g = the Element of H as Element of G by GROUP_2:42;
assume x in the carrier of G ; :: thesis: x in union ()
then reconsider a = x as Element of G ;
A1: a = a * (1_ G) by GROUP_1:def 4
.= a * ((g ") * g) by GROUP_1:def 5
.= (a * (g ")) * g by GROUP_1:def 3 ;
A2: (a * (g ")) * H in Cosets H by GROUP_2:def 15;
the Element of H in H by STRUCT_0:def 5;
then a in (a * (g ")) * H by ;
hence x in union () by ; :: thesis: verum
end;
then A3: the carrier of G c= union () ;
Cosets N = Cosets H by Def14;
hence union () = the carrier of G by ; :: thesis: verum