theorem Th6: :: FUNCT_7:6

for f being Function
for a being set st a in dom f holds
f | {a} = a .--> (f . a)