now

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

end;

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