let A be finite set ; :: thesis: (canFS A) " is Function of A, Seg (card A)
len (canFS A) = card A by Def1;
then A2: dom (canFS A) = Seg (card A) by FINSEQ_1:def 3;
rng (canFS A) = A by FUNCT_2:def 3;
then A3: dom ((canFS A) " ) = A by FUNCT_1:55;
rng ((canFS A) " ) = Seg (card A) by A2, FUNCT_1:55;
hence (canFS A) " is Function of A, Seg (card A) by A3, FUNCT_2:3; :: thesis: verum