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:57;
thus rng (f | {X}) c= {(f . X)} by Th96; :: according to XBOOLE_0:def 10 :: thesis: {(f . X)} c= rng (f | {X})
let x be object ; :: 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, Th46;
hence x in rng (f | {X}) by A2, Def3; :: thesis: verum