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