let X be non empty set ; :: thesis: for Y being set
for f being Function of X,{Y} holds rng f = {Y}
let Y be set ; :: thesis: for f being Function of X,{Y} holds rng f = {Y}
let f be Function of X,{Y}; :: thesis: rng f = {Y}
thus rng f c= {Y} ; :: according to XBOOLE_0:def 10 :: thesis: {Y} c= rng f
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {Y} or q in rng f )
consider x being object such that
A1: x in X by XBOOLE_0:def 1;
assume q in {Y} ; :: thesis: q in rng f
then A2: ( dom f = X & q = Y ) by FUNCT_2:def 1, TARSKI:def 1;
f . x = Y by A1, FUNCT_2:50;
hence q in rng f by A2, A1, FUNCT_1:def 3; :: thesis: verum