let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being MSAlgebra of S st U1 is strict MSSubAlgebra of U2 & U2 is strict MSSubAlgebra of U1 holds
U1 = U2
let U1, U2 be MSAlgebra of S; :: thesis: ( U1 is strict MSSubAlgebra of U2 & U2 is strict MSSubAlgebra of U1 implies U1 = U2 )
assume A1:
( U1 is strict MSSubAlgebra of U2 & U2 is strict MSSubAlgebra of U1 )
; :: thesis: U1 = U2
then
( the Sorts of U1 is MSSubset of U2 & the Sorts of U2 is MSSubset of U1 )
by Def10;
then
( the Sorts of U1 c= the Sorts of U2 & the Sorts of U2 c= the Sorts of U1 )
by PBOOLE:def 23;
then A2:
the Sorts of U1 = the Sorts of U2
by PBOOLE:def 13;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A1, Def10;
reconsider B2 = the Sorts of U2 as MSSubset of U1 by A1, Def10;
A3:
( B2 is opers_closed & the Charact of U2 = Opers U1,B2 & B1 is opers_closed & the Charact of U1 = Opers U2,B1 )
by A1, Def10;
set O = the Charact of U1;
set P = Opers U1,B2;
for x being set st x in the carrier' of S holds
the Charact of U1 . x = (Opers U1,B2) . x
proof
let x be
set ;
:: thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers U1,B2) . x )
assume
x in the
carrier' of
S
;
:: thesis: the Charact of U1 . x = (Opers U1,B2) . x
then reconsider o =
x as
OperSymbol of
S ;
A4:
B1 is_closed_on o
by A3, Def7;
A5:
Args o,
U2 = ((B2 # ) * the Arity of S) . o
by MSUALG_1:def 9;
thus the
Charact of
U1 . x =
o /. B1
by A3, Def9
.=
(Den o,U2) | (((B1 # ) * the Arity of S) . o)
by A4, Def8
.=
Den o,
U2
by A2, A5, RELSET_1:34
.=
(Opers U1,B2) . x
by A3, MSUALG_1:def 11
;
:: thesis: verum
end;
hence
U1 = U2
by A1, A2, A3, PBOOLE:3; :: thesis: verum