let f be NAT * -defined to-naturals homogeneous Function; :: thesis: arity <*f*> = arity f
rng <*f*> = {f} by FINSEQ_1:38;
then f in rng <*f*> by TARSKI:def 1;
hence arity <*f*> = arity f by Def4; :: thesis: verum