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;
then rng p c= NAT by XBOOLE_1:1;
hence k --> m is XFinSequence of ; :: thesis: verum