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

reconsider g = the Element of H as Element of G by Th42;

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 object ; :: 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 ;

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 A3, Th104;

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

( 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

set h = the Element of H;
set h = the Element of H;

reconsider g = the Element of H as Element of G by Th42;

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 object ; :: 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 ;

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 A1, Th103;

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

end;reconsider g = the Element of H as Element of G by Th42;

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 object ; :: 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 ;

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 A1, Th103;

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

reconsider g = the Element of H as Element of G by Th42;

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 object ; :: 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 ;

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 A3, Th104;

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