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 Th55;
thus rightker (RQ*Form f) c= {(0. (VectQuot (W,(RKer (f *')))))} :: according to XBOOLE_0:def 10,BILINEAR:def 24 :: thesis: K160( the carrier of (VectQuot (W,(RKer (f *')))),(0. (VectQuot (W,(RKer (f *')))))) c= rightker (RQ*Form f)

proof

let x be object ; :: 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:22;

now :: thesis: for v being Vector of V holds f . (v,w) = 0. F_Complex

let v be Vector of V; :: thesis: f . (v,w) = 0. F_Complex
thus f . (v,w) = (RQ*Form f) . (v,ww) by A4, Th59
.= 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 19;
then w in RKer (f *') by STRUCT_0:def 5;
then w + (RKer (f *')) = zeroCoset (W,(RKer (f *'))) by VECTSP_4:49
.= 0. (VectQuot (W,(RKer (f *')))) by VECTSP10:21 ;
hence x in {(0. (VectQuot (W,(RKer (f *')))))} by A2, A4, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K160( 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:29;
hence x in rightker (RQ*Form f) by A5; :: thesis: verum