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