thus rng (f |^ a) c= NAT by VALUED_0:def 6; :: according to FINSEQ_1:def 4 :: thesis: verum