let X be set ; :: thesis: for x being object
for f being Function st x in X & x in dom f holds
f . x in f .: X
let x be object ; :: 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
A1: x in X and
A2: x in dom f ; :: thesis: f . x in f .: X
x in X /\ (dom f) by A1, A2, XBOOLE_0:def 4;
then x in dom (f | X) by RELAT_1:61;
then A3: (f | X) . x in rng (f | X) by Def3;
(f | X) . x = f . x by A1, Th48;
hence f . x in f .: X by A3, RELAT_1:115; :: thesis: verum