A1:
the ResultSort of (MSSign A) = (dom (signature A)) --> 0
by Def13;
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 Def13;
len (signature A) = len the charact of A
by UNIALG_1:def 11;
then A3:
dom the charact of A = OS
by A2, FINSEQ_3:31;
then reconsider O = the charact of A as ManySortedSet of OS by PARTFUN1:def 4, RELAT_1:def 18;
A4:
the Arity of (MSSign A) = (*--> 0 ) * (signature A)
by Def13;
reconsider O = O as ManySortedFunction of OS ;
A5:
the carrier of (MSSign A) = {0 }
by Def13;
O is ManySortedFunction of DO,RO
proof
set D = the
carrier of
A;
let i be
set ;
PBOOLE:def 18 ( 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, UNIALG_1:5, UNIALG_1:def 5;
n in dom ((dom (signature A)) --> 0 )
by A2, A7, FUNCOP_1:19;
then RO . i =
(MSSorts A) . (((dom (signature A)) --> 0 ) . n)
by A1, FUNCT_1:23
.=
({0 } --> the carrier of A) . 0
by A2, A7, FUNCOP_1:13
.=
the
carrier of
A
by A6, FUNCOP_1:13
;
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:55
.=
((M # ) * (*--> 0 )) . ((signature A) . n)
by A5, A2, A7, FUNCT_1:23
.=
((M # ) * (*--> 0 )) . (arity h)
by A2, A7, UNIALG_1:def 11
.=
Funcs (Seg (arity h)),the
carrier of
A
by PBOOLE:153
.=
dom (O . o)
by Th8
;
hence
O . i is
Element of
K10(
K11(
(DO . i),
(RO . i)))
by A8, FUNCT_2:def 1, RELSET_1:11;
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