let G be addGroup; :: 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
set h = the Element of H;
reconsider g = the Element of H as Element of G by Th41, STRUCT_0:def 5;
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 + (0_ G) by Def4
.= a + ((- g) + g) by Def5
.= (a + (- g)) + g by RLVECT_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;
set h = the Element of H;
reconsider g = the Element of H as Element of G by Th41, STRUCT_0:def 5;
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 = (0_ G) + a by Def4
.= (g + (- g)) + a by Def5
.= g + ((- g) + a) by RLVECT_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