A1:
the ResultSort of (MSSign A) = (dom (signature A)) --> 0
by Def8;
reconsider OS = the carrier' of (MSSign A) as non empty set ;
reconsider DO = ((MSSorts A) #) * the Arity of (MSSign A), RO = (MSSorts A) * the ResultSort of (MSSign A) as ManySortedSet of OS ;
A2:
the carrier' of (MSSign A) = dom (signature A)
by Def8;
len (signature A) = len the charact of A
by UNIALG_1:def 4;
then A3:
dom the charact of A = OS
by A2, FINSEQ_3:29;
then reconsider O = the charact of A as ManySortedSet of OS by PARTFUN1:def 2, RELAT_1:def 18;
A4:
the Arity of (MSSign A) = (*--> 0) * (signature A)
by Def8;
reconsider O = O as ManySortedFunction of OS ;
A5:
the carrier of (MSSign A) = {0}
by Def8;
O is ManySortedFunction of DO,RO
proof
set D = the
carrier of
A;
let i be
object ;
PBOOLE:def 15 ( not i in OS or O . i is Element of K10(K11((DO . i),(RO . i))) )
reconsider M =
0 .--> the
carrier of
A as
ManySortedSet of
{0} ;
A6:
0 in {0}
by TARSKI:def 1;
assume A7:
i in OS
;
O . i is Element of K10(K11((DO . i),(RO . i)))
then reconsider n =
i as
Nat by A2;
reconsider h =
O . n as non
empty homogeneous quasi_total PartFunc of
( the carrier of A *), the
carrier of
A by A3, A7, MARGREL1:def 24, UNIALG_1:1;
n in dom ((dom (signature A)) --> 0)
by A2, A7;
then RO . i =
(MSSorts A) . (((dom (signature A)) --> 0) . n)
by A1, FUNCT_1:13
.=
({0} --> the carrier of A) . 0
by A2, A7, FUNCOP_1:7
.=
the
carrier of
A
by A6, FUNCOP_1:7
;
then A8:
rng h c= RO . i
by RELAT_1:def 19;
reconsider o =
i as
Element of
OS by A7;
DO . i =
((((MSSorts A) #) * (*--> 0)) * (signature A)) . n
by A4, RELAT_1:36
.=
((M #) * (*--> 0)) . ((signature A) . n)
by A5, A2, A7, FUNCT_1:13
.=
((M #) * (*--> 0)) . (arity h)
by A2, A7, UNIALG_1:def 4
.=
Funcs (
(Seg (arity h)), the
carrier of
A)
by FINSEQ_2:145
.=
dom (O . o)
by Th3
;
hence
O . i is
Element of
K10(
K11(
(DO . i),
(RO . i)))
by A8, FUNCT_2:def 1, RELSET_1:4;
verum
end;
hence
the charact of A is ManySortedFunction of ((MSSorts A) #) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A)
; verum