let U1, U2 be Universal_Algebra; :: thesis: ( U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2 )
assume that
A1: U1 is strict SubAlgebra of U2 and
A2: U2 is strict SubAlgebra of U1 ; :: thesis: U1 = U2
reconsider B = the carrier of U1 as non empty Subset of U2 by A1, Def7;
the carrier of U2 c= the carrier of U2 ;
then reconsider B1 = the carrier of U2 as non empty Subset of U2 ;
A3: dom (Opers (U2,B1)) = dom the charact of U2 by Def6;
A4: for n being Nat st n in dom the charact of U2 holds
the charact of U2 . n = (Opers (U2,B1)) . n

proof

let n be Nat; :: thesis: ( n in dom the charact of U2 implies the charact of U2 . n = (Opers (U2,B1)) . n )
assume A5: n in dom the charact of U2 ; :: thesis: the charact of U2 . n = (Opers (U2,B1)) . n
then reconsider o = the charact of U2 . n as operation of U2 by FUNCT_1:def 3;
(Opers (U2,B1)) . n = o /. B1 by A3, A5, Def6
.= o by Th4 ;
hence the charact of U2 . n = (Opers (U2,B1)) . n ; :: thesis: verum

end;

the carrier of U2 is Subset of U1 by A2, Def7;
then A6: B1 = B ;
then the charact of U1 = Opers (U2,B1) by A1, Def7;
hence U1 = U2 by A1, A2, A6, A3, A4, FINSEQ_1:13; :: thesis: verum