reconsider f = f as LinearOperator of X,Y by Def7;
f . v is VECTOR of Y ;
hence f . v is VECTOR of Y ; :: thesis: verum