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 23 :: thesis: {(0. (VectQuot (V,(LKer f))))} c= 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 Th30;

hence x in leftker (LQForm f) by A4; :: thesis: verum

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 23 :: thesis: {(0. (VectQuot (V,(LKer f))))} c= leftker (LQForm f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. (VectQuot (V,(LKer f))))} or x in leftker (LQForm f) )
let x be object ; :: 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:22;

then v in the carrier of (LKer f) by Def18;

then v in LKer f ;

then v + (LKer f) = the carrier of (LKer f) by VECTSP_4:49

.= zeroCoset (V,(LKer f)) by VECTSP10:def 4

.= 0. (VectQuot (V,(LKer f))) by VECTSP10:21 ;

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

end;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:22;

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

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

thus f . (v,w) = (LQForm f) . (vv,w) by A3, Def20

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

end;thus f . (v,w) = (LQForm f) . (vv,w) by A3, Def20

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

then v in the carrier of (LKer f) by Def18;

then v in LKer f ;

then v + (LKer f) = the carrier of (LKer f) by VECTSP_4:49

.= zeroCoset (V,(LKer f)) by VECTSP10:def 4

.= 0. (VectQuot (V,(LKer f))) by VECTSP10:21 ;

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

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

hence x in leftker (LQForm f) by A4; :: thesis: verum