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 Lm6;

Cosets N = Cosets H by Def14;

hence union (Cosets N) = the carrier of G by A3, XBOOLE_0:def 10; :: thesis: verum

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 Lm6;

now :: thesis: for x being object st x in the carrier of G holds

x in union (Cosets H)

then A3:
the carrier of G c= union (Cosets H)
;x in union (Cosets H)

set h = the Element of H;

let x be object ; :: thesis: ( x in the carrier of G implies x in union (Cosets H) )

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 (Cosets H)

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 A1, GROUP_2:103;

hence x in union (Cosets H) by A2, TARSKI:def 4; :: thesis: verum

end;let x be object ; :: thesis: ( x in the carrier of G implies x in union (Cosets H) )

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 (Cosets H)

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 A1, GROUP_2:103;

hence x in union (Cosets H) by A2, TARSKI:def 4; :: thesis: verum

Cosets N = Cosets H by Def14;

hence union (Cosets N) = the carrier of G by A3, XBOOLE_0:def 10; :: thesis: verum