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