for L being non empty multMagma
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