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

( 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