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

proof

thus union (Left_Cosets H) c= the carrier of G ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= union (Left_Cosets H)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of G or x in union (Left_Cosets H) )
assume x in the carrier of G ; :: thesis: x in union (Left_Cosets H)
then reconsider a = x as Element of G ;
consider h being Element of H;
reconsider g = h as Element of G by Th51;
A1: h in H by STRUCT_0:def 5;
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 ;
then ( a in (a * (g " )) * H & (a * (g " )) * H in Left_Cosets H ) by A1, Def15, Th125;
hence x in union (Left_Cosets H) by TARSKI:def 4; :: thesis: verum

end;

thus union (Right_Cosets H) c= the carrier of G ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= union (Right_Cosets H)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of G or x in union (Right_Cosets H) )
assume x in the carrier of G ; :: thesis: x in union (Right_Cosets H)
then reconsider a = x as Element of G ;
consider h being Element of H;
reconsider g = h as Element of G by Th51;
A2: h in H by STRUCT_0:def 5;
a = (1_ G) * a by GROUP_1:def 5
.= (g * (g " )) * a by GROUP_1:def 6
.= g * ((g " ) * a) by GROUP_1:def 4 ;
then ( a in H * ((g " ) * a) & H * ((g " ) * a) in Right_Cosets H ) by A2, Def16, Th126;
hence x in union (Right_Cosets H) by TARSKI:def 4; :: thesis: verum