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;
reconsider Fx = F . x as finite set ;
x in dom F by A1, CARD_3:def 2;
then y = card Fx by A2, 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