let MS be non empty trivial non void segmental ManySortedSign ; for A being non-empty MSAlgebra of MS holds the Charact of A is FinSequence of PFuncs ((the_sort_of A) * ),(the_sort_of A)
let A be non-empty MSAlgebra of MS; the Charact of A is FinSequence of PFuncs ((the_sort_of A) * ),(the_sort_of A)
A1:
dom the Charact of A = the carrier' of MS
by PARTFUN1:def 4;
ex n being Element of NAT st the carrier' of MS = Seg n
then reconsider f = the Charact of A as FinSequence by A1, FINSEQ_1:def 2;
f is FinSequence of PFuncs ((the_sort_of A) * ),(the_sort_of A)
proof
let x be
set ;
TARSKI:def 3,
FINSEQ_1:def 4 ( not x in proj2 f or x in PFuncs ((the_sort_of A) * ),(the_sort_of A) )
assume
x in rng f
;
x in PFuncs ((the_sort_of A) * ),(the_sort_of A)
then consider i being
set such that A3:
i in the
carrier' of
MS
and A4:
f . i = x
by A1, FUNCT_1:def 5;
reconsider i =
i as
OperSymbol of
MS by A3;
A5:
the
Sorts of
A . (the ResultSort of MS . i) is
Component of the
Sorts of
A
by PBOOLE:151;
dom the
ResultSort of
MS = the
carrier' of
MS
by FUNCT_2:def 1;
then (the Sorts of A * the ResultSort of MS) . i =
the
Sorts of
A . (the ResultSort of MS . i)
by FUNCT_1:23
.=
the_sort_of A
by A5, Def17
;
then A6:
x is
Function of
(Args i,A),
(the_sort_of A)
by A4, PBOOLE:def 18;
Args i,
A c= (the_sort_of A) *
by Th13;
then
x is
PartFunc of
((the_sort_of A) * ),
(the_sort_of A)
by A6, RELSET_1:17;
hence
x in PFuncs ((the_sort_of A) * ),
(the_sort_of A)
by PARTFUN1:119;
verum
end;
hence
the Charact of A is FinSequence of PFuncs ((the_sort_of A) * ),(the_sort_of A)
; verum