let L be 1-sorted ; :: thesis: 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 #)

let A, B be AlgebraStr over L; :: thesis: ( 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 ; :: thesis: 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:68, ZFMISC_1:96 ;

A8: ( 0. A = 0. B & 1. A = 1. B ) by A1, Def3;

A9: the multF of A = the multF of B || the carrier of A by A1, Def3

.= the multF of B by A5 ;

the addF of A = the addF of B || the carrier of A by A1, Def3

.= the addF of B by A5 ;

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, A9, A7, A8, XBOOLE_0:def 10; :: thesis: verum

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 over L; :: thesis: ( 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 ; :: thesis: 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:68, ZFMISC_1:96 ;

A8: ( 0. A = 0. B & 1. A = 1. B ) by A1, Def3;

A9: the multF of A = the multF of B || the carrier of A by A1, Def3

.= the multF of B by A5 ;

the addF of A = the addF of B || the carrier of A by A1, Def3

.= the addF of B by A5 ;

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, A9, A7, A8, XBOOLE_0:def 10; :: thesis: verum