rightker (RQForm f) = {(0. (VectQuot (W,(RKer f))))} by Def24;
then A1: rightker (LQForm (RQForm f)) = {(0. (VectQuot (W,(RKer f))))} by Th44;
leftker (LQForm f) = {(0. (VectQuot (V,(LKer f))))} by Def23;
then A2: leftker (RQForm (LQForm f)) = {(0. (VectQuot (V,(LKer f))))} by Th45;
( leftker (RQForm (LQForm f)) = leftker (QForm f) & rightker (LQForm (RQForm f)) = rightker (QForm f) ) by Th49;
hence ( not QForm f is degenerated-on-left & not QForm f is degenerated-on-right ) by A2, A1; :: thesis: verum