theorem :: COMPUT_1:43

for f being NAT * -defined to-naturals homogeneous Function holds arity <*f*> = arity f