let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1, g2 being Element of G
for h1, h2 being Element of H1 st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G
for g1, g2 being Element of G
for h1, h2 being Element of H1 st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
let H1 be StableSubgroup of G; :: thesis: for g1, g2 being Element of G
for h1, h2 being Element of H1 st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
let g1, g2 be Element of G; :: thesis: for h1, h2 being Element of H1 st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
let h1, h2 be Element of H1; :: thesis: ( h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2 )
assume A1: ( h1 = g1 & h2 = g2 ) ; :: thesis: h1 * h2 = g1 * g2
H1 is Subgroup of G by Def7;
hence h1 * h2 = g1 * g2 by A1, GROUP_2:43; :: thesis: verum