theorem Th26: :: GRFUNC_1:28

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