theorem Th25: :: PARTFUN1:25

for x being object
for X, Y being set
for f being Function st x in dom f & x in X & f . x in Y holds
<:f,X,Y:> . x = f . x