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