let X be set ; :: thesis: for x being object
for f being Function st x in dom (f | X) holds
(f | X) . x = f . x
let x be object ; :: thesis: for f being Function st x in dom (f | X) holds
(f | X) . x = f . x
let f be Function; :: thesis: ( x in dom (f | X) implies (f | X) . x = f . x )
set g = f | X;
assume A1: x in dom (f | X) ; :: thesis: (f | X) . x = f . x
dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A2: x in dom f by A1, XBOOLE_0:def 4;
( f | X c= f & [x,((f | X) . x)] in f | X ) by A1, Def2, RELAT_1:59;
hence (f | X) . x = f . x by A2, Def2; :: thesis: verum