let G be addGroup; :: thesis: for a, b being Element of G
for H being Subgroup of G holds (H + a) + b c= (H + a) + (H + b)
let a, b be Element of G; :: thesis: for H being Subgroup of G holds (H + a) + b c= (H + a) + (H + b)
let H be Subgroup of G; :: thesis: (H + a) + b c= (H + a) + (H + b)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (H + a) + b or x in (H + a) + (H + b) )
A1: (0_ G) + b in H + b by Th46, Th104;
assume x in (H + a) + b ; :: thesis: x in (H + a) + (H + b)
then x in H + (a + b) by ThB34;
then consider g being Element of G such that
A2: x = g + (a + b) and
A3: g in H by Th104;
A4: x = (g + a) + b by A2, RLVECT_1:def 3
.= (g + a) + ((0_ G) + b) by Def4 ;
g + a in H + a by A3, Th104;
hence x in (H + a) + (H + b) by A1, A4; :: thesis: verum