let x, X be set ; :: thesis: for f being Function st x in dom f & x in X holds
f . x in rng (f | X)
let f be Function; :: thesis: ( x in dom f & x in X implies f . x in rng (f | X) )
assume A1: ( x in dom f & x in X ) ; :: thesis: f . x in rng (f | X)
then x in (dom f) /\ X by XBOOLE_0:def 4;
then ( x in dom (f | X) & (f | X) . x = f . x ) by A1, RELAT_1:90, Th72;
hence f . x in rng (f | X) by Def5; :: thesis: verum