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