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 finite-yielding 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

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;

then rng (NAT --> {}) c= bool NAT ;
hence NAT --> {} is natsubset-yielding ; :: thesis: verum