let G be non empty addGroup-like addMagma ; :: thesis: for g1, g2 being Element of G
for H being Subgroup of G
for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 + h2 = g1 + g2
let g1, g2 be Element of G; :: thesis: for H being Subgroup of G
for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 + h2 = g1 + g2
let H be Subgroup of G; :: thesis: for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 + h2 = g1 + g2
let h1, h2 be Element of H; :: thesis: ( h1 = g1 & h2 = g2 implies h1 + h2 = g1 + g2 )
assume A1: ( h1 = g1 & h2 = g2 ) ; :: thesis: h1 + h2 = g1 + g2
h1 + h2 = ( the addF of G || the carrier of H) . [h1,h2] by DefA5;
hence h1 + h2 = g1 + g2 by A1, FUNCT_1:49; :: thesis: verum