let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis:
let V, W be VectSp of K; :: thesis:
let f be bilinear-Form of V,W; :: thesis:
set vq = VectQuot (V,(LKer f));
set wq = VectQuot (W,(RKer f));
set wqr = VectQuot (W,(RKer (LQForm f)));
set vql = VectQuot (V,(LKer (RQForm f)));
set rlf = RQForm (LQForm f);
set qf = QForm f;
set lrf = LQForm (RQForm f);
thus leftker (QForm f) c= leftker (RQForm (LQForm f)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in leftker (QForm f) ; :: thesis:
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A1: x = vv and
A2: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K ;

now :: thesis:

let ww be Vector of (VectQuot (W,(RKer (LQForm f)))); :: thesis:
reconsider w = ww as Vector of (VectQuot (W,(RKer f))) by Th46;
thus (RQForm (LQForm f)) . (vv,ww) = (QForm f) . (vv,w) by Th48
.= 0. K by A2 ; :: thesis:

end;

hence x in leftker (RQForm (LQForm f)) by A1; :: thesis:

end;

thus leftker (RQForm (LQForm f)) c= leftker (QForm f) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in leftker (RQForm (LQForm f)) ; :: thesis:
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A3: x = vv and
A4: for ww being Vector of (VectQuot (W,(RKer (LQForm f)))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K ;

now :: thesis:

let ww be Vector of (VectQuot (W,(RKer f))); :: thesis:
reconsider w = ww as Vector of (VectQuot (W,(RKer (LQForm f)))) by Th46;
thus (QForm f) . (vv,ww) = (RQForm (LQForm f)) . (vv,w) by Th48
.= 0. K by A4 ; :: thesis:

end;

hence x in leftker (QForm f) by A3; :: thesis:

end;

thus rightker (QForm f) c= rightker (RQForm (LQForm f)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rightker (QForm f) ; :: thesis:
then consider ww being Vector of (VectQuot (W,(RKer f))) such that
A5: x = ww and
A6: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K ;
reconsider w = ww as Vector of (VectQuot (W,(RKer (LQForm f)))) by Th46;

now :: thesis:

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis:
thus (RQForm (LQForm f)) . (vv,w) = (QForm f) . (vv,ww) by Th48
.= 0. K by A6 ; :: thesis:

end;

hence x in rightker (RQForm (LQForm f)) by A5; :: thesis:

end;

thus rightker (RQForm (LQForm f)) c= rightker (QForm f) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rightker (RQForm (LQForm f)) ; :: thesis:
then consider ww being Vector of (VectQuot (W,(RKer (LQForm f)))) such that
A7: x = ww and
A8: for vv being Vector of (VectQuot (V,(LKer f))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K ;
reconsider w = ww as Vector of (VectQuot (W,(RKer f))) by Th46;

now :: thesis:

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis:
thus (QForm f) . (vv,w) = (RQForm (LQForm f)) . (vv,ww) by Th48
.= 0. K by A8 ; :: thesis:

end;

hence x in rightker (QForm f) by A7; :: thesis:

end;

thus leftker (QForm f) c= leftker (LQForm (RQForm f)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in leftker (QForm f) ; :: thesis:
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A9: x = vv and
A10: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K ;
reconsider v = vv as Vector of (VectQuot (V,(LKer (RQForm f)))) by Th47;

now :: thesis:

let ww be Vector of (VectQuot (W,(RKer f))); :: thesis:
thus (LQForm (RQForm f)) . (v,ww) = (QForm f) . (vv,ww) by Th48
.= 0. K by A10 ; :: thesis:

end;

hence x in leftker (LQForm (RQForm f)) by A9; :: thesis:

end;

thus leftker (LQForm (RQForm f)) c= leftker (QForm f) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in leftker (LQForm (RQForm f)) ; :: thesis:
then consider vv being Vector of (VectQuot (V,(LKer (RQForm f)))) such that
A11: x = vv and
A12: for ww being Vector of (VectQuot (W,(RKer f))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K ;
reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th47;

now :: thesis:

let ww be Vector of (VectQuot (W,(RKer f))); :: thesis:
thus (QForm f) . (v,ww) = (LQForm (RQForm f)) . (vv,ww) by Th48
.= 0. K by A12 ; :: thesis:

end;

hence x in leftker (QForm f) by A11; :: thesis:

end;

thus rightker (QForm f) c= rightker (LQForm (RQForm f)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rightker (QForm f) ; :: thesis:
then consider ww being Vector of (VectQuot (W,(RKer f))) such that
A13: x = ww and
A14: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K ;

now :: thesis:

let vv be Vector of (VectQuot (V,(LKer (RQForm f)))); :: thesis:
reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th47;
thus (LQForm (RQForm f)) . (vv,ww) = (QForm f) . (v,ww) by Th48
.= 0. K by A14 ; :: thesis:

end;

hence x in rightker (LQForm (RQForm f)) by A13; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rightker (LQForm (RQForm f)) ; :: thesis:
then consider ww being Vector of (VectQuot (W,(RKer f))) such that
A15: x = ww and
A16: for vv being Vector of (VectQuot (V,(LKer (RQForm f)))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K ;

now :: thesis:

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis:
reconsider v = vv as Vector of (VectQuot (V,(LKer (RQForm f)))) by Th47;
thus (QForm f) . (vv,ww) = (LQForm (RQForm f)) . (v,ww) by Th48
.= 0. K by A16 ; :: thesis:

end;

hence x in rightker (QForm f) by A15; :: thesis: