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

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