let X be set ; :: thesis: for f being Function st X in dom f holds
rng (f | {X}) = {(f . X)}
let f be Function; :: thesis: ( X in dom f implies rng (f | {X}) = {(f . X)} )
A1: X in {X} by TARSKI:def 1;
assume X in dom f ; :: thesis: rng (f | {X}) = {(f . X)}
then A2: X in dom (f | {X}) by A1, RELAT_1:86;
thus rng (f | {X}) c= {(f . X)} by Th167; :: according to XBOOLE_0:def 10 :: thesis: {(f . X)} c= rng (f | {X})
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f . X)} or x in rng (f | {X}) )
assume x in {(f . X)} ; :: thesis: x in rng (f | {X})
then x = f . X by TARSKI:def 1;
then x = (f | {X}) . X by A2, Th70;
hence x in rng (f | {X}) by A2, Def5; :: thesis: verum