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 by FUNCT_2:52;
hence rng f c= dom f ; :: thesis: verum