f . x in rng f by FUNCT_1:3;
hence f . x is Element of R ; :: thesis: verum