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