set F = NAT --> {} ;
A1: ( dom (NAT --> {} ) = NAT & rng (NAT --> {} ) = {{} } ) by FUNCOP_1:14, FUNCOP_1:19;
take NAT --> {} ; :: thesis: ( NAT --> {} is finite-yielding & NAT --> {} is natsubset-yielding )

now

let x be set ; :: thesis: ( x in rng (NAT --> {} ) implies x in bool NAT )
assume A2: x in rng (NAT --> {} ) ; :: thesis: x in bool NAT
x = {} by A1, A2, TARSKI:def 1;
then x c= NAT by XBOOLE_1:2;
hence x in bool NAT ; :: thesis: verum

end;

then A3: rng (NAT --> {} ) c= bool NAT by TARSKI:def 3;
for x being set st x in rng (NAT --> {} ) holds
x is finite ;
hence NAT --> {} is finite-yielding by Lm2; :: thesis: NAT --> {} is natsubset-yielding
thus NAT --> {} is natsubset-yielding by A3, Def3; :: thesis: verum