consider g being Function such that
A1: f = g and
A2: dom g = X and
A3: rng g c= the carrier of Y by FUNCT_2:def 2;
f . x in rng g by A1, A2, FUNCT_1:def 3;
hence f . x is VECTOR of Y by A3; :: thesis: verum