let x be object ; :: thesis: for X being set
for f being Function st x in rng f holds
rng (f +* (X --> x)) c= rng f
let X be set ; :: thesis: for f being Function st x in rng f holds
rng (f +* (X --> x)) c= rng f
let f be Function; :: thesis: ( x in rng f implies rng (f +* (X --> x)) c= rng f )
assume x in rng f ; :: thesis: rng (f +* (X --> x)) c= rng f
then (rng f) \/ {x} = rng f by ZFMISC_1:40;
then A1: (rng f) \/ (rng (X --> x)) c= rng f by XBOOLE_1:9;
rng (f +* (X --> x)) c= (rng f) \/ (rng (X --> x)) by FUNCT_4:17;
hence rng (f +* (X --> x)) c= rng f by A1, XBOOLE_1:1; :: thesis: verum