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

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