dom f = Seg (len f) by FINSEQ_1:def 3;
hence findom f is Element of Fin NAT by FINSUB_1:def 5; :: thesis: verum