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