consider F being Function such that
A1: dom F = 1 and
A2: rng F = {1} by FUNCT_1:5;
take F ; :: thesis: ( not F is empty & F is finite-yielding )

now

let x be set ; :: thesis: F . b₁ is finite

per cases ( x in dom F or not x in dom F ) ;

suppose x in dom F ; :: thesis: F . b₁ is finite

then F . x in rng F by FUNCT_1:def 3;
hence F . x is finite by A2; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: F . b₁ is finite

hence F . x is finite by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence ( not F is empty & F is finite-yielding ) by A1, Def3; :: thesis: verum