let A be finite set ; :: thesis: canFS A is ManySortedSet of Seg (card A)
set f = canFS A;
len (canFS A) = card A by FINSEQ_1:93;
then A1: dom (canFS A) = Seg (card A) by FINSEQ_1:def 3;
then reconsider f = canFS A as Seg (card A) -defined Function by RELAT_1:def 18;
f is total by A1, PARTFUN1:def 2;
hence canFS A is ManySortedSet of Seg (card A) ; :: thesis: verum