theorem Th7: :: GRFUNC_1:7

for x being object
for f being Function st dom f = {x} holds
f = {[x,(f . x)]}