f . x in rng f by FUNCT_2:6;
hence f . x is Element of Y ; :: thesis: verum