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