let L be 1-sorted ; for A, B being AlgebraStr of 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 #)
let A, B be AlgebraStr of L; ( A is Subalgebra of B & B is Subalgebra of A implies 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 #) )
assume that
A1:
A is Subalgebra of B
and
A2:
B is Subalgebra of A
; 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 #)
A3:
the carrier of B c= the carrier of A
by A2, Def3;
A4:
the carrier of A c= the carrier of B
by A1, Def3;
then A5:
the carrier of A = the carrier of B
by A3, XBOOLE_0:def 10;
A6:
dom the lmult of B = [:the carrier of L,the carrier of B:]
by Th2;
A7: the lmult of A =
the lmult of B | [:the carrier of L,the carrier of A:]
by A1, Def3
.=
the lmult of B
by A3, A6, RELAT_1:97, ZFMISC_1:119
;
A8:
dom the addF of B = [:the carrier of B,the carrier of B:]
by Th1;
A9:
( 0. A = 0. B & 1. A = 1. B )
by A1, Def3;
A10:
dom the multF of B = [:the carrier of B,the carrier of B:]
by Th1;
A11: the multF of A =
the multF of B || the carrier of A
by A1, Def3
.=
the multF of B
by A5, A10, RELAT_1:97
;
the addF of A =
the addF of B || the carrier of A
by A1, Def3
.=
the addF of B
by A5, A8, RELAT_1:97
;
hence
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 #)
by A4, A3, A11, A7, A9, XBOOLE_0:def 10; verum