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