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