theorem :: PBOOLE:2

for f being Function holds
( f is empty-yielding iff ( f = {} or rng f = {{}} ) )