set qf = RQForm f;
set R = RKer f;
set qW = VectQuot W,(RKer f);
thus rightker (RQForm f) c= {(0. (VectQuot W,(RKer f)))} :: according to XBOOLE_0:def 10,BILINEAR:def 25 :: thesis: {(0. (VectQuot W,(RKer f)))} c= rightker (RQForm f)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (RQForm f) or x in {(0. (VectQuot W,(RKer f)))} )
assume x in rightker (RQForm f) ; :: thesis: x in {(0. (VectQuot W,(RKer f)))}
then consider ww being Vector of (VectQuot W,(RKer f)) such that
A1: ( x = ww & ( for v being Vector of V holds (RQForm f) . v,ww = 0. K ) ) ;
consider w being Vector of W such that
A2: ww = w + (RKer f) by VECTSP10:23;

now

let v be Vector of V; :: thesis: f . v,w = 0. K
thus f . v,w = (RQForm f) . v,ww by A2, Def22
.= 0. K by A1 ; :: thesis: verum

end;

then w in rightker f ;
then w in the carrier of (RKer f) by Def20;
then w in RKer f by STRUCT_0:def 5;
then w + (RKer f) = the carrier of (RKer f) by VECTSP_4:64
.= zeroCoset W,(RKer f) by VECTSP10:def 4
.= 0. (VectQuot W,(RKer f)) by VECTSP10:22 ;
hence x in {(0. (VectQuot W,(RKer f)))} by A1, A2, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. (VectQuot W,(RKer f)))} or x in rightker (RQForm f) )
assume x in {(0. (VectQuot W,(RKer f)))} ; :: thesis: x in rightker (RQForm f)
then A3: x = 0. (VectQuot W,(RKer f)) by TARSKI:def 1;
for v being Vector of V holds (RQForm f) . v,(0. (VectQuot W,(RKer f))) = 0. K by Th30;
hence x in rightker (RQForm f) by A3; :: thesis: verum