theorem
for
L being
1-sorted for
A,
B being
AlgebraStr over
L st
A is
Subalgebra of
B &
B is
Subalgebra of
A holds
AlgebraStr(# the
carrier of
A, the
addF of
A, the
multF of
A, the
ZeroF of
A, the
OneF of
A, the
lmult of
A #)
= AlgebraStr(# the
carrier of
B, the
addF of
B, the
multF of
B, the
ZeroF of
B, the
OneF of
B, the
lmult of
B #)