theorem :: GRFUNC_1:21

for f being Function st f = {} holds
f " = {}