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:40;

reconsider B = w + (RKer (f *')) as Vector of (VectQuot (W,(RKer (f *')))) by VECTSP10:23;

reconsider A = v + (LKer f) as Vector of (VectQuot (V,(LKer f))) by VECTSP10:23;

(Q*Form f) . (A,B) = f . (v,w) by Def12;

hence not Q*Form f is constant by A1, BILINEAR:40; :: thesis: verum

consider v being Vector of V, w being Vector of W such that

A1: f . (v,w) <> 0. F_Complex by BILINEAR:40;

reconsider B = w + (RKer (f *')) as Vector of (VectQuot (W,(RKer (f *')))) by VECTSP10:23;

reconsider A = v + (LKer f) as Vector of (VectQuot (V,(LKer f))) by VECTSP10:23;

(Q*Form f) . (A,B) = f . (v,w) by Def12;

hence not Q*Form f is constant by A1, BILINEAR:40; :: thesis: verum