now

A1: n is Subset of NAT by Th8;
let y be set ; :: thesis: ( y in f " x implies y in NAT )
assume y in f " x ; :: thesis: y in NAT
hence y in NAT by A1, TARSKI:def 3; :: thesis: verum

end;

hence f " x is Subset of NAT by TARSKI:def 3; :: thesis: verum