theorem Th85: :: FUNCT_4:85

for a, b being set
for f being Function st a in dom f & f . a = b holds
a .--> b c= f