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