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 )
assume x in (dom f) /\ X ; :: thesis: (f | X) . x = f . x
then x in dom (f | X) by RELAT_1:61;
hence (f | X) . x = f . x by Th46; :: thesis: verum