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

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