reconsider f = f as BilinearOperator of X,Y,Z by Def9;
f . (v,w) is VECTOR of Z ;
hence f . (v,w) is VECTOR of Z ; :: thesis: verum