let X be set ; :: thesis: for f being Function of X,X holds rng f c= dom f
let f be Function of X,X; :: thesis: rng f c= dom f
( dom f = X & rng f c= X ) by FUNCT_2:67;
hence rng f c= dom f ; :: thesis: verum