let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G
for a, b being Element of H
for a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b'
let H be non empty SubStr of G; :: thesis: for a, b being Element of H
for a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b'
let a, b be Element of H; :: thesis: for a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b'
let a', b' be Element of G; :: thesis: ( a = a' & b = b' implies a * b = a' * b' )
assume A1: ( a = a' & b = b' ) ; :: thesis: a * b = a' * b'
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]
.= a' * b' by A1, A2, GRFUNC_1:8 ; :: thesis: verum