let U1, U2 be Universal_Algebra; :: thesis: ( U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2 )
assume A1: ( U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 ) ; :: thesis: U1 = U2
then A2: the carrier of U2 is Subset of U1 by Def8;
reconsider B = the carrier of U1 as non empty Subset of U2 by A1, Def8;
the carrier of U2 c= the carrier of U2 ;
then reconsider B1 = the carrier of U2 as non empty Subset of U2 ;
A3: B1 = B by A2, XBOOLE_0:def 10;
then A4: ( the charact of U1 = Opers U2,B1 & B1 is opers_closed ) by A1, Def8;
A5: dom (Opers U2,B1) = dom the charact of U2 by Def7;
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 A6: 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 5;
(Opers U2,B1) . n = o /. B1 by A5, A6, Def7
.= o by Th7 ;
hence the charact of U2 . n = (Opers U2,B1) . n ; :: thesis: verum

end;

hence U1 = U2 by A1, A3, A4, A5, FINSEQ_1:17; :: thesis: verum