let X be set ; :: thesis: for x being object
for f being Function st x in X holds
(f | X) . x = f . x
let x be object ; :: thesis: for f being Function st x in X holds
(f | X) . x = f . x
let f be Function; :: thesis: ( x in X implies (f | X) . x = f . x )
assume A1: x in X ; :: thesis: (f | X) . x = f . x

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: (f | X) . x = f . x

then x in dom (f | X) by A1, RELAT_1:57;
hence (f | X) . x = f . x by Th46; :: thesis: verum

end;

suppose A2: not x in dom f ; :: thesis: (f | X) . x = f . x

then not x in dom (f | X) by RELAT_1:57;
hence (f | X) . x = {} by Def2
.= f . x by A2, Def2 ;
:: thesis: verum

end;

end;