let A be finite set ; :: thesis: len (canFS A) = card A
rng (canFS A) = A by FUNCT_2:def 3;
hence len (canFS A) = card A by FINSEQ_4:77; :: thesis: verum