let x, X be set ; :: 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;
A2: dom (f | X) = (dom f) /\ X by RELAT_1:90;
A3: f | X c= f by RELAT_1:88;
assume A4: x in dom (f | X) ; :: thesis: (f | X) . x = f . x
then A5: [x,((f | X) . x)] in f | X by Def4;
x in dom f by A2, A4, XBOOLE_0:def 4;
hence (f | X) . x = f . x by A3, A5, Def4; :: thesis: verum