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 OS by PBOOLE:def 3;
reconsider O = O as ManySortedFunction of OS ;
reconsider DO = ((MSSorts A) # ) * the Arity of (MSSign A), RO = (MSSorts A) * the ResultSort of (MSSign A) as ManySortedSet of OS ;
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 M5(DO . i,RO . i) )
assume A3:
i in OS
;
:: thesis: O . i is M5(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;
dom (0 .--> the carrier of A) = {0 }
by FUNCOP_1:19;
then reconsider M =
0 .--> the
carrier of
A as
ManySortedSet of
{0 } by PBOOLE:def 3;
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
;
A7:
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 RELSET_1:12;
hence
O . i is
Function of
DO . i,
RO . i
by A6, A7, 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