let MS be non void 1 -element segmental ManySortedSign ; for A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
let A be non-empty MSAlgebra over 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 2;
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
object ;
TARSKI:def 3,
FINSEQ_1:def 4 ( not x in rng 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
object such that A3:
i in the
carrier' of
MS
and A4:
f . i = x
by A1, FUNCT_1:def 3;
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:139;
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:13
.=
the_sort_of A
by A5, Def12
;
then A6:
x is
Function of
(Args (i,A)),
(the_sort_of A)
by A4, PBOOLE:def 15;
Args (
i,
A)
c= (the_sort_of A) *
by Th7;
then
x is
PartFunc of
((the_sort_of A) *),
(the_sort_of A)
by A6, RELSET_1:7;
hence
x in PFuncs (
((the_sort_of A) *),
(the_sort_of A))
by PARTFUN1:45;
verum
end;
hence
the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
; verum