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)

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

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 K160( the carrier of (VectQuot (W,(RKer (f *')))),(0. (VectQuot (W,(RKer (f *')))))) or x in rightker (RQ*Form f) )
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;

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;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

then
w in rightker f
;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;thus f . (v,w) = (RQ*Form f) . (v,ww) by A4, Th59

.= 0. F_Complex by A3 ; :: thesis: verum

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

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