let S be non empty non void ManySortedSign ; for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
let U1, U2 be MSAlgebra over S; ( U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
assume that
A1:
U1 is MSSubAlgebra of U2
and
A2:
U2 is MSSubAlgebra of U1
; MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
the Sorts of U2 is MSSubset of U1
by A2, Def9;
then A3:
the Sorts of U2 c= the Sorts of U1
by PBOOLE:def 18;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A1, Def9;
A4:
the Charact of U1 = Opers (U2,B1)
by A1, Def9;
reconsider B2 = the Sorts of U2 as MSSubset of U1 by A2, Def9;
A5:
the Charact of U2 = Opers (U1,B2)
by A2, Def9;
the Sorts of U1 is MSSubset of U2
by A1, Def9;
then
the Sorts of U1 c= the Sorts of U2
by PBOOLE:def 18;
then A6:
the Sorts of U1 = the Sorts of U2
by A3, PBOOLE:146;
set O = the Charact of U1;
set P = Opers (U1,B2);
A7:
B1 is opers_closed
by A1, Def9;
for x being object st x in the carrier' of S holds
the Charact of U1 . x = (Opers (U1,B2)) . x
proof
let x be
object ;
( x in the carrier' of S implies the Charact of U1 . x = (Opers (U1,B2)) . x )
assume
x in the
carrier' of
S
;
the Charact of U1 . x = (Opers (U1,B2)) . x
then reconsider o =
x as
OperSymbol of
S ;
A8:
Args (
o,
U2)
= ((B2 #) * the Arity of S) . o
by MSUALG_1:def 4;
A9:
B1 is_closed_on o
by A7;
thus the
Charact of
U1 . x =
o /. B1
by A4, Def8
.=
(Den (o,U2)) | (((B1 #) * the Arity of S) . o)
by A9, Def7
.=
Den (
o,
U2)
by A6, A8
.=
(Opers (U1,B2)) . x
by A5, MSUALG_1:def 6
;
verum
end;
hence
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
by A6, A5, PBOOLE:3; verum