dom (k --> m) = k by FUNCOP_1:19;
then reconsider p = k --> m as XFinSequence by AFINSQ_1:7;
rng p c= {m} by FUNCOP_1:19;
hence k --> m is XFinSequence of NAT ; :: thesis: verum