let G be non empty Group-like multMagma ; :: 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 multF of G || the carrier of H) . [h1,h2] by Def5;
hence h1 * h2 = g1 * g2 by A1, FUNCT_1:49; :: thesis: verum