let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G
for a, b being Element of H
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let H be non empty SubStr of G; :: thesis: for a, b being Element of H
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let a, b be Element of H; :: thesis: for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let a9, b9 be Element of G; :: thesis: ( a = a9 & b = b9 implies a * b = a9 * b9 )
assume A1: ( a = a9 & b = b9 ) ; :: thesis: a * b = a9 * b9
A2: ( dom H₂(H) = [:H₁(H),H₁(H):] & H₂(H) c= H₂(G) ) by Def23, FUNCT_2:def 1;
thus a * b = H₂(H) . [a,b]
.= a9 * b9 by A1, A2, GRFUNC_1:2 ; :: thesis: verum