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 addF of B || the carrier of A) . [x9,y9] by A1, FUNCT_1:49
.= x9 + y9 by Def3 ;
:: thesis: verum