let S, E be non void Signature; for A being non-empty disjoint_valued MSAlgebra of S st A is MSAlgebra of E holds
ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #) = ManySortedSign(# the carrier of E,the carrier' of E,the Arity of E,the ResultSort of E #)
let A be non-empty disjoint_valued MSAlgebra of S; ( A is MSAlgebra of E implies ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #) = ManySortedSign(# the carrier of E,the carrier' of E,the Arity of E,the ResultSort of E #) )
A1:
dom the Sorts of A = the carrier of S
by PARTFUN1:def 4;
assume A2:
A is MSAlgebra of E
; ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #) = ManySortedSign(# the carrier of E,the carrier' of E,the Arity of E,the ResultSort of E #)
then reconsider B = A as MSAlgebra of E ;
A3:
the carrier of S = the carrier of E
by A2, Th62;
A5:
now let x be
set ;
( x in the carrier' of S implies the ResultSort of S . x = the ResultSort of E . x )assume
x in the
carrier' of
S
;
the ResultSort of S . x = the ResultSort of E . xthen reconsider o =
x as
OperSymbol of
S ;
reconsider e =
o as
OperSymbol of
E by A2, Th62;
consider p being
Element of
Args o,
A;
Den e,
B = the
Charact of
B . e
;
then A6:
rng (Den o,A) c= Result e,
B
by RELAT_1:def 19;
(Den o,A) . p in rng (Den o,A)
by FUNCT_2:6;
then
Result o,
A meets Result e,
B
by A6, XBOOLE_0:3;
then Result o,
A =
(the Sorts of B * the ResultSort of E) . x
by Th64
.=
the
Sorts of
B . (the ResultSort of E . e)
by FUNCT_2:21
;
then
the
Sorts of
A . (the ResultSort of E . e) = the
Sorts of
A . (the ResultSort of S . o)
by FUNCT_2:21;
hence
the
ResultSort of
S . x = the
ResultSort of
E . x
by A3, A1, FUNCT_1:def 8;
verum end;
A7:
now let x be
set ;
( x in the carrier' of S implies the Arity of S . x = the Arity of E . x )assume
x in the
carrier' of
S
;
the Arity of S . x = the Arity of E . xthen reconsider o =
x as
OperSymbol of
S ;
reconsider e =
o as
OperSymbol of
E by A2, Th62;
reconsider p = the
Arity of
E . e as
Element of the
carrier of
E * ;
reconsider q = the
Arity of
S . o as
Element of the
carrier of
S * ;
Den e,
B = the
Charact of
B . e
;
then A8:
dom (Den o,A) = Args e,
B
by FUNCT_2:def 1;
dom (Den o,A) = Args o,
A
by FUNCT_2:def 1;
then Args o,
A =
(the Sorts of B # ) . p
by A8, FUNCT_2:21
.=
product (the Sorts of B * p)
by PBOOLE:def 19
;
then product (the Sorts of A * p) =
(the Sorts of A # ) . q
by FUNCT_2:21
.=
product (the Sorts of A * q)
by PBOOLE:def 19
;
then A9:
the
Sorts of
B * p = the
Sorts of
A * q
by PUA2MSS1:2;
A10:
rng q c= the
carrier of
S
;
then A11:
dom (the Sorts of A * q) = dom q
by A1, RELAT_1:46;
A12:
rng p c= the
carrier of
E
;
then
dom (the Sorts of B * p) = dom p
by A3, A1, RELAT_1:46;
hence
the
Arity of
S . x = the
Arity of
E . x
by A3, A1, A9, A12, A10, A11, FUNCT_1:49;
verum end;
A13:
dom the Arity of E = the carrier' of E
by FUNCT_2:def 1;
A14:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
A15:
dom the ResultSort of E = the carrier' of E
by FUNCT_2:def 1;
A16:
the carrier' of S = the carrier' of E
by A2, Th62;
dom the ResultSort of S = the carrier' of S
by FUNCT_2:def 1;
then
the ResultSort of S = the ResultSort of E
by A2, A15, A5, Th62, FUNCT_1:9;
hence
ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #) = ManySortedSign(# the carrier of E,the carrier' of E,the Arity of E,the ResultSort of E #)
by A3, A16, A14, A13, A7, FUNCT_1:9; verum