rng (Card F) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Card F) or y in NAT )
assume y in rng (Card F) ; :: thesis: y in NAT
then consider x being object such that
A1: x in dom (Card F) and
A2: y = (Card F) . x by FUNCT_1:def 3;
A3: x in dom F by A1, CARD_3:def 2;
then F . x in rng F by FUNCT_1:3;
then reconsider Fx = F . x as finite set ;
y = card Fx by A2, A3, CARD_3:def 2;
hence y in NAT ; :: thesis: verum

end;

hence Card F is Cardinal-yielding FinSequence of NAT by FINSEQ_1:def 4; :: thesis: verum