let Y, x, X be set ; :: thesis: for f being Y -valued Function st x in dom (f | X) holds
(f | X) /. x = f /. x
let f be Y -valued Function; :: thesis: ( x in dom (f | X) implies (f | X) /. x = f /. x )
assume Z: x in dom (f | X) ; :: thesis: (f | X) /. x = f /. x
then A: x in dom f by RELAT_1:57;
thus (f | X) /. x = (f | X) . x by Z, Def6
.= f . x by Z, FUNCT_1:47
.= f /. x by A, Def6 ; :: thesis: verum