let S, E be non void Signature; :: thesis: 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; :: thesis: ( 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 #) )
assume A1:
A is MSAlgebra of E
; :: thesis: 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 ;
A2:
( the carrier of S = the carrier of E & the carrier' of S = the carrier' of E )
by A1, Th62;
A3:
( the Sorts of A is one-to-one & dom the Sorts of A = the carrier of S )
by Th63, PARTFUN1:def 4;
A4:
( dom the ResultSort of S = the carrier' of S & dom the ResultSort of E = the carrier' of E )
by FUNCT_2:def 1;
now let x be
set ;
:: thesis: ( x in the carrier' of S implies the ResultSort of S . x = the ResultSort of E . x )assume
x in the
carrier' of
S
;
:: thesis: 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 A1, Th62;
consider p being
Element of
Args o,
A;
(
Den o,
A = the
Charact of
A . o &
Den e,
B = the
Charact of
B . e )
;
then
(
rng (Den o,A) c= Result o,
A &
rng (Den o,A) c= Result e,
B &
(Den o,A) . p in rng (Den o,A) )
by FUNCT_2:6, RELAT_1:def 19;
then
Result o,
A meets Result e,
B
by 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 A2, A3, FUNCT_1:def 8;
:: thesis: verum end;
then A5:
the ResultSort of S = the ResultSort of E
by A1, Th62, A4, FUNCT_1:9;
A6:
( dom the Arity of S = the carrier' of S & dom the Arity of E = the carrier' of E )
by FUNCT_2:def 1;
now let x be
set ;
:: thesis: ( x in the carrier' of S implies the Arity of S . x = the Arity of E . x )assume
x in the
carrier' of
S
;
:: thesis: 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 A1, 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 o,
A = the
Charact of
A . o &
Den e,
B = the
Charact of
B . e &
Result e,
B is
Component of the
Sorts of
A )
;
then
(
dom (Den o,A) = Args o,
A &
dom (Den o,A) = Args e,
B )
by FUNCT_2:def 1;
then Args o,
A =
(the Sorts of B # ) . p
by 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 A7:
the
Sorts of
B * p = the
Sorts of
A * q
by PUA2MSS1:2;
A8:
(
rng p c= the
carrier of
E &
rng q c= the
carrier of
S )
;
then
(
dom (the Sorts of B * p) = dom p &
dom (the Sorts of A * q) = dom q )
by A2, A3, RELAT_1:46;
hence
the
Arity of
S . x = the
Arity of
E . x
by A2, A3, A7, A8, FUNCT_1:49;
:: thesis: verum end;
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 A2, A5, A6, FUNCT_1:9; :: thesis: verum