let S, E be non void Signature; for A being non-empty disjoint_valued MSAlgebra over S st A is MSAlgebra over 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 over S; ( A is MSAlgebra over 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 2;
assume A2:
A is MSAlgebra over 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 over E ;
A3:
the carrier of S = the carrier of E
by A2, Th60;
A4:
now for x being object st x in the carrier' of S holds
the ResultSort of S . x = the ResultSort of E . xlet x be
object ;
( 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, Th60;
set p = the
Element of
Args (
o,
A);
Den (
e,
B)
= the
Charact of
B . e
;
then A5:
rng (Den (o,A)) c= Result (
e,
B)
by RELAT_1:def 19;
(Den (o,A)) . the
Element of
Args (
o,
A)
in rng (Den (o,A))
by FUNCT_2:4;
then
Result (
o,
A)
meets Result (
e,
B)
by A5, XBOOLE_0:3;
then Result (
o,
A) =
( the Sorts of B * the ResultSort of E) . x
by Th61
.=
the
Sorts of
B . ( the ResultSort of E . e)
by FUNCT_2:15
;
then
the
Sorts of
A . ( the ResultSort of E . e) = the
Sorts of
A . ( the ResultSort of S . o)
by FUNCT_2:15;
hence
the
ResultSort of
S . x = the
ResultSort of
E . x
by A3, A1, FUNCT_1:def 4;
verum end;
A6:
now for x being object st x in the carrier' of S holds
the Arity of S . x = the Arity of E . xlet x be
object ;
( 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, Th60;
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 A7:
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 A7, FUNCT_2:15
.=
product ( the Sorts of B * p)
by FINSEQ_2:def 5
;
then product ( the Sorts of A * p) =
( the Sorts of A #) . q
by FUNCT_2:15
.=
product ( the Sorts of A * q)
by FINSEQ_2:def 5
;
then A8:
the
Sorts of
B * p = the
Sorts of
A * q
by PUA2MSS1:2;
A9:
rng q c= the
carrier of
S
;
then A10:
dom ( the Sorts of A * q) = dom q
by A1, RELAT_1:27;
A11:
rng p c= the
carrier of
E
;
then
dom ( the Sorts of B * p) = dom p
by A3, A1, RELAT_1:27;
hence
the
Arity of
S . x = the
Arity of
E . x
by A3, A1, A8, A11, A9, A10, FUNCT_1:27;
verum end;
A12:
dom the Arity of E = the carrier' of E
by FUNCT_2:def 1;
A13:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
the ResultSort of S = the ResultSort of E
by A2, A4, Th60;
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, A13, A12, A6, FUNCT_1:2; verum