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

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

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

the carrier of U2 is Subset of U1
by A2, Def7;
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;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

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