set K = F_Complex ;
consider v being Vector of V, w being Vector of W such that
A1: f . v,w <> 0. F_Complex by BILINEAR:41;
reconsider B = w + (RKer (f *' )) as Vector of (VectQuot W,(RKer (f *' ))) by VECTSP10:24;
reconsider A = v + (LKer f) as Vector of (VectQuot V,(LKer f)) by VECTSP10:24;
(Q*Form f) . A,B = f . v,w by Def12;
hence not Q*Form f is constant by A1, BILINEAR:41; :: thesis: verum