set F = NAT --> {};

take NAT --> {} ; :: thesis: ( NAT --> {} is finite-yielding & NAT --> {} is natsubset-yielding )

for x being set st x in rng (NAT --> {}) holds

x is finite ;

hence NAT --> {} is V50() by FINSET_1:def 2; :: thesis: NAT --> {} is natsubset-yielding

hence NAT --> {} is natsubset-yielding ; :: thesis: verum

take NAT --> {} ; :: thesis: ( NAT --> {} is finite-yielding & NAT --> {} is natsubset-yielding )

for x being set st x in rng (NAT --> {}) holds

x is finite ;

hence NAT --> {} is V50() by FINSET_1:def 2; :: thesis: NAT --> {} is natsubset-yielding

now :: thesis: for x being object st x in rng (NAT --> {}) holds

x in bool NAT

then
rng (NAT --> {}) c= bool NAT
;x in bool NAT

let x be object ; :: thesis: ( x in rng (NAT --> {}) implies x in bool NAT )

reconsider xx = x as set by TARSKI:1;

assume x in rng (NAT --> {}) ; :: thesis: x in bool NAT

then x = {} by TARSKI:def 1;

then xx c= NAT ;

hence x in bool NAT ; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in rng (NAT --> {}) ; :: thesis: x in bool NAT

then x = {} by TARSKI:def 1;

then xx c= NAT ;

hence x in bool NAT ; :: thesis: verum

hence NAT --> {} is natsubset-yielding ; :: thesis: verum