theorem Th7: :: COMPUT_1:7

for f being Function-yielding Function st {} in rng f holds
<:f:> = {}