reconsider OS = the carrier' of (MSSign A) as non empty set ;
A1:
( the carrier of (MSSign A) = {0 } & the carrier' of (MSSign A) = dom (signature A) & the Arity of (MSSign A) = (*--> 0 ) * (signature A) & the ResultSort of (MSSign A) = (dom (signature A)) --> 0 )
by Def13;
len (signature A) = len the charact of A
by UNIALG_1:def 11;
then A2:
dom the charact of A = OS
by A1, FINSEQ_3:31;
then reconsider O = the charact of A as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
reconsider O = O as ManySortedFunction of ;
reconsider DO = ((MSSorts A) # ) * the Arity of (MSSign A), RO = (MSSorts A) * the ResultSort of (MSSign A) as ManySortedSet of ;
O is ManySortedFunction of DO,RO
proof
let i be
set ;
:: according to PBOOLE:def 18 :: thesis: ( not i in OS or O . i is Element of K10(K11((DO . i),(RO . i))) )
assume A3:
i in OS
;
:: thesis: O . i is Element of K10(K11((DO . i),(RO . i)))
then reconsider o =
i as
Element of
OS ;
reconsider n =
i as
Nat by A1, A3;
set D = the
carrier of
A;
reconsider h =
O . n as non
empty homogeneous quasi_total PartFunc of
(the carrier of A * ),the
carrier of
A by A2, A3, UNIALG_1:5, UNIALG_1:def 5;
reconsider M =
0 .--> the
carrier of
A as
ManySortedSet of ;
A4:
n in dom ((dom (signature A)) --> 0 )
by A1, A3, FUNCOP_1:19;
A5:
0 in {0 }
by TARSKI:def 1;
A6:
DO . i =
((((MSSorts A) # ) * (*--> 0 )) * (signature A)) . n
by A1, RELAT_1:55
.=
((M # ) * (*--> 0 )) . ((signature A) . n)
by A1, A3, FUNCT_1:23
.=
((M # ) * (*--> 0 )) . (arity h)
by A1, A3, UNIALG_1:def 11
.=
Funcs (Seg (arity h)),the
carrier of
A
by PBOOLE:153
.=
dom (O . o)
by Th8
;
RO . i =
(MSSorts A) . (((dom (signature A)) --> 0 ) . n)
by A1, A4, FUNCT_1:23
.=
({0 } --> the carrier of A) . 0
by A1, A3, FUNCOP_1:13
.=
the
carrier of
A
by A5, FUNCOP_1:13
;
then
rng h c= RO . i
by RELAT_1:def 19;
hence
O . i is
Element of
K10(
K11(
(DO . i),
(RO . i)))
by A6, FUNCT_2:def 1, RELSET_1:11;
:: thesis: verum
end;
hence
the charact of A is ManySortedFunction of ((MSSorts A) # ) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A)
; :: thesis: verum