set K = F_Complex ;
set qf = RQ*Form f;
set R = RKer (f *' );
set qW = VectQuot W,(RKer (f *' ));
A1: rightker f = rightker (f *' ) by Th58;
thus rightker (RQ*Form f) c= {(0. (VectQuot W,(RKer (f *' ))))} :: according to XBOOLE_0:def 10,BILINEAR:def 25 :: thesis: K195(the carrier of (VectQuot W,(RKer (f *' ))),(0. (VectQuot W,(RKer (f *' ))))) c= rightker (RQ*Form f)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (RQ*Form f) or x in {(0. (VectQuot W,(RKer (f *' ))))} )
assume x in rightker (RQ*Form f) ; :: thesis: x in {(0. (VectQuot W,(RKer (f *' ))))}
then consider ww being Vector of (VectQuot W,(RKer (f *' ))) such that
A2: x = ww and
A3: for v being Vector of V holds (RQ*Form f) . v,ww = 0. F_Complex ;
consider w being Vector of W such that
A4: ww = w + (RKer (f *' )) by VECTSP10:23;

now

let v be Vector of V; :: thesis: f . v,w = 0. F_Complex
thus f . v,w = (RQ*Form f) . v,ww by A4, Th62
.= 0. F_Complex by A3 ; :: thesis: verum

end;

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K195(the carrier of (VectQuot W,(RKer (f *' ))),(0. (VectQuot W,(RKer (f *' ))))) or x in rightker (RQ*Form f) )
assume x in {(0. (VectQuot W,(RKer (f *' ))))} ; :: thesis: x in rightker (RQ*Form f)
then A5: x = 0. (VectQuot W,(RKer (f *' ))) by TARSKI:def 1;
for v being Vector of V holds (RQ*Form f) . v,(0. (VectQuot W,(RKer (f *' )))) = 0. F_Complex by BILINEAR:30;
hence x in rightker (RQ*Form f) by A5; :: thesis: verum