rightker (RQForm f) = {(0. (VectQuot W,(RKer f)))} by Def25;
then rightker (LQForm (RQForm f)) = {(0. (VectQuot W,(RKer f)))} by Th45;
hence ( not LQForm (RQForm f) is degenerated-on-left & not LQForm (RQForm f) is degenerated-on-right ) by Def25; :: thesis: verum