let X be set ; :: thesis: for f being Function holds rng (f | {X}) c= {(f . X)}
let f be Function; :: thesis: rng (f | {X}) c= {(f . X)}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f | {X}) or x in {(f . X)} )
assume x in rng (f | {X}) ; :: thesis: x in {(f . X)}
then consider y being object such that
A1: y in dom (f | {X}) and
A2: x = (f | {X}) . y by Def3;
dom (f | {X}) c= {X} by RELAT_1:58;
then y = X by A1, TARSKI:def 1;
then x = f . X by A1, A2, Th46;
hence x in {(f . X)} by TARSKI:def 1; :: thesis: verum