let MS be non void 1 -element segmental ManySortedSign ; :: thesis: 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; :: thesis: 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

proof

consider n being Nat such that
A2: the carrier' of MS = Seg n by Def7;
n in NAT by ORDINAL1:def 12;
hence ex n being Element of NAT st the carrier' of MS = Seg n by A2; :: thesis: verum

end;

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 ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not x in rng f or x in PFuncs (((the_sort_of A) *),(the_sort_of A)) )
assume x in rng f ; :: thesis: 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; :: thesis: verum

end;

hence the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A)) ; :: thesis: verum