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