let G be addGroup; :: thesis: for a being Element of G
for H being Subgroup of G holds (2 * a) + H c= (a + H) + (a + H)
let a be Element of G; :: thesis: for H being Subgroup of G holds (2 * a) + H c= (a + H) + (a + H)
let H be Subgroup of G; :: thesis: (2 * a) + H c= (a + H) + (a + H)
(2 * a) + H = (a + a) + H by Th26;
hence (2 * a) + H c= (a + H) + (a + H) by Th116; :: thesis: verum