let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B
for a being Element of L
for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
let B be non empty AlgebraStr over L; :: thesis: for A being non empty Subalgebra of B
for a being Element of L
for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
let A be non empty Subalgebra of B; :: thesis: for a being Element of L
for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
let a be Element of L; :: thesis: for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
let x be Element of B; :: thesis: for x9 being Element of A st x = x9 holds
a * x = a * x9
let x9 be Element of A; :: thesis: ( x = x9 implies a * x = a * x9 )
assume A1: x = x9 ; :: thesis: a * x = a * x9
[a,x9] in [: the carrier of L, the carrier of A:] by ZFMISC_1:87;
hence a * x = ( the lmult of B | [: the carrier of L, the carrier of A:]) . [a,x9] by A1, FUNCT_1:49
.= a * x9 by Def3 ;
:: thesis: verum