rng (Card F) c= NAT

proof

hence
Card F is Cardinal-yielding FinSequence of NAT
by FINSEQ_1:def 4; :: thesis: verum
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;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