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