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 24 :: thesis: {(0. (VectQuot (W,(RKer f))))} c= rightker (RQForm f)

assume x in {(0. (VectQuot (W,(RKer f))))} ; :: thesis: x in rightker (RQForm f)

then A4: 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 Th29;

hence x in rightker (RQForm f) by A4; :: thesis: verum

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 24 :: thesis: {(0. (VectQuot (W,(RKer f))))} c= rightker (RQForm f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. (VectQuot (W,(RKer f))))} or x in rightker (RQForm f) )
let x be object ; :: 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 and

A2: for v being Vector of V holds (RQForm f) . (v,ww) = 0. K ;

consider w being Vector of W such that

A3: ww = w + (RKer f) by VECTSP10:22;

then w in the carrier of (RKer f) by Def19;

then w in RKer f ;

then w + (RKer f) = the carrier of (RKer f) by VECTSP_4:49

.= zeroCoset (W,(RKer f)) by VECTSP10:def 4

.= 0. (VectQuot (W,(RKer f))) by VECTSP10:21 ;

hence x in {(0. (VectQuot (W,(RKer f))))} by A1, A3, TARSKI:def 1; :: thesis: verum

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

A2: for v being Vector of V holds (RQForm f) . (v,ww) = 0. K ;

consider w being Vector of W such that

A3: ww = w + (RKer f) by VECTSP10:22;

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

then
w in rightker f
;let v be Vector of V; :: thesis: f . (v,w) = 0. K

thus f . (v,w) = (RQForm f) . (v,ww) by A3, Def21

.= 0. K by A2 ; :: thesis: verum

end;thus f . (v,w) = (RQForm f) . (v,ww) by A3, Def21

.= 0. K by A2 ; :: thesis: verum

then w in the carrier of (RKer f) by Def19;

then w in RKer f ;

then w + (RKer f) = the carrier of (RKer f) by VECTSP_4:49

.= zeroCoset (W,(RKer f)) by VECTSP10:def 4

.= 0. (VectQuot (W,(RKer f))) by VECTSP10:21 ;

hence x in {(0. (VectQuot (W,(RKer f))))} by A1, A3, TARSKI:def 1; :: thesis: verum

assume x in {(0. (VectQuot (W,(RKer f))))} ; :: thesis: x in rightker (RQForm f)

then A4: 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 Th29;

hence x in rightker (RQForm f) by A4; :: thesis: verum