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