set qf = LQForm f;
set L = LKer f;
set qV = VectQuot V,(LKer f);
thus leftker (LQForm f) c= {(0. (VectQuot V,(LKer f)))} :: according to XBOOLE_0:def 10,BILINEAR:def 24 :: thesis: {(0. (VectQuot V,(LKer f)))} c= leftker (LQForm f)

proof

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

now

let w be Vector of W; :: thesis: f . v,w = 0. K
thus f . v,w = (LQForm f) . vv,w by A3, Def21
.= 0. K by A2 ; :: thesis: verum

end;

then v in leftker f ;
then v in the carrier of (LKer f) by Def19;
then v in LKer f by STRUCT_0:def 5;
then v + (LKer f) = the carrier of (LKer f) by VECTSP_4:64
.= zeroCoset V,(LKer f) by VECTSP10:def 4
.= 0. (VectQuot V,(LKer f)) by VECTSP10:22 ;
hence x in {(0. (VectQuot V,(LKer f)))} by A1, A3, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. (VectQuot V,(LKer f)))} or x in leftker (LQForm f) )
assume x in {(0. (VectQuot V,(LKer f)))} ; :: thesis: x in leftker (LQForm f)
then A4: x = 0. (VectQuot V,(LKer f)) by TARSKI:def 1;
for w being Vector of W holds (LQForm f) . (0. (VectQuot V,(LKer f))),w = 0. K by Th31;
hence x in leftker (LQForm f) by A4; :: thesis: verum