let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr of L
for A being non empty Subalgebra of B
for x, y being Element of B
for x', y' being Element of A st x = x' & y = y' holds
x * y = x' * y'
let B be non empty AlgebraStr of L; :: thesis: for A being non empty Subalgebra of B
for x, y being Element of B
for x', y' being Element of A st x = x' & y = y' holds
x * y = x' * y'
let A be non empty Subalgebra of B; :: thesis: for x, y being Element of B
for x', y' being Element of A st x = x' & y = y' holds
x * y = x' * y'
let x, y be Element of B; :: thesis: for x', y' being Element of A st x = x' & y = y' holds
x * y = x' * y'
let x', y' be Element of A; :: thesis: ( x = x' & y = y' implies x * y = x' * y' )
assume A1: ( x = x' & y = y' ) ; :: thesis: x * y = x' * y'
[x',y'] in [:the carrier of A,the carrier of A:] by ZFMISC_1:106;
hence x * y = (the multF of B || the carrier of A) . [x',y'] by A1, FUNCT_1:72
.= x' * y' by Def3 ;
:: thesis: verum