A1: ( leftker (RQ*Form (LQForm f)) = {(0. (VectQuot (V,(LKer f))))} & rightker (LQForm (RQ*Form f)) = {(0. (VectQuot (W,(RKer (f *')))))} ) by BILINEAR:def 23, BILINEAR:def 24;
( leftker (RQ*Form (LQForm f)) = leftker (Q*Form f) & rightker (LQForm (RQ*Form f)) = rightker (Q*Form f) ) by Th64;
hence ( not Q*Form f is degenerated-on-left & not Q*Form f is degenerated-on-right ) by A1; :: thesis: verum