let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr over L

for A being non empty Subalgebra of B

for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

let B be non empty AlgebraStr over L; :: thesis: for A being non empty Subalgebra of B

for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

let A be non empty Subalgebra of B; :: thesis: for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

let x, y be Element of B; :: thesis: for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

let x9, y9 be Element of A; :: thesis: ( x = x9 & y = y9 implies x * y = x9 * y9 )

assume A1: ( x = x9 & y = y9 ) ; :: thesis: x * y = x9 * y9

[x9,y9] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87;

hence x * y = ( the multF of B || the carrier of A) . [x9,y9] by A1, FUNCT_1:49

.= x9 * y9 by Def3 ;

:: thesis: verum

for A being non empty Subalgebra of B

for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

let B be non empty AlgebraStr over L; :: thesis: for A being non empty Subalgebra of B

for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

let A be non empty Subalgebra of B; :: thesis: for x, y being Element of B

for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

let x, y be Element of B; :: thesis: for x9, y9 being Element of A st x = x9 & y = y9 holds

x * y = x9 * y9

let x9, y9 be Element of A; :: thesis: ( x = x9 & y = y9 implies x * y = x9 * y9 )

assume A1: ( x = x9 & y = y9 ) ; :: thesis: x * y = x9 * y9

[x9,y9] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87;

hence x * y = ( the multF of B || the carrier of A) . [x9,y9] by A1, FUNCT_1:49

.= x9 * y9 by Def3 ;

:: thesis: verum