let G be Group; :: thesis: for H being Subgroup of G holds
( union () = the carrier of G & union () = the carrier of G )

let H be Subgroup of G; :: thesis: ( union () = the carrier of G & union () = the carrier of G )
thus union () = the carrier of G :: thesis: union () = the carrier of G
proof
set h = the Element of H;
reconsider g = the Element of H as Element of G by Th42;
thus union () c= the carrier of G ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= union ()
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of G or x in union () )
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 Left_Cosets H by Def15;
the Element of H in H ;
then a in (a * (g ")) * H by ;
hence x in union () by ; :: thesis: verum
end;
set h = the Element of H;
reconsider g = the Element of H as Element of G by Th42;
thus union () c= the carrier of G ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= union ()
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of G or x in union () )
assume x in the carrier of G ; :: thesis: x in union ()
then reconsider a = x as Element of G ;
A3: a = (1_ G) * a by GROUP_1:def 4
.= (g * (g ")) * a by GROUP_1:def 5
.= g * ((g ") * a) by GROUP_1:def 3 ;
A4: H * ((g ") * a) in Right_Cosets H by Def16;
the Element of H in H ;
then a in H * ((g ") * a) by ;
hence x in union () by ; :: thesis: verum