let x be object ; :: thesis: for X, Y being set
for f being b₂ -valued Function st x in dom (f | X) holds
(f | X) /. x = f /. x
let X, Y 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 A1: x in dom (f | X) ; :: thesis: (f | X) /. x = f /. x
then A2: x in dom f by RELAT_1:57;
thus (f | X) /. x = (f | X) . x by A1, Def6
.= f . x by A1, FUNCT_1:47
.= f /. x by A2, Def6 ; :: thesis: verum