reconsider TfS = denomi-set f as non empty finite Subset of NAT ;
rng (canFS TfS) c= NAT by ORDINAL1:def 12;
hence canFS (denomi-set f) is non empty FinSequence of NAT by FINSEQ_1:def 4; :: thesis: verum