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