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