let G be addGroup; :: thesis: for H being Subgroup of G holds (carr H) + (carr H) = carr H
let H be Subgroup of G; :: thesis: (carr H) + (carr H) = carr H
A1: for g being Element of G st g in carr H holds
- g in carr H by Th75;
for g1, g2 being Element of G st g1 in carr H & g2 in carr H holds
g1 + g2 in carr H by Th74;
hence (carr H) + (carr H) = carr H by A1, Th22; :: thesis: verum