let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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 set ; :: 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

let ww be Vector of (VectQuot W,(RKer (LQForm f))); :: thesis:
reconsider w = ww as Vector of (VectQuot W,(RKer f)) by Th47;
thus (RQForm (LQForm f)) . vv,ww = (QForm f) . vv,w by Th49
.= 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 set ; :: 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

let ww be Vector of (VectQuot W,(RKer f)); :: thesis:
reconsider w = ww as Vector of (VectQuot W,(RKer (LQForm f))) by Th47;
thus (QForm f) . vv,ww = (RQForm (LQForm f)) . vv,w by Th49
.= 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 set ; :: 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 Th47;

now

let vv be Vector of (VectQuot V,(LKer f)); :: thesis:
thus (RQForm (LQForm f)) . vv,w = (QForm f) . vv,ww by Th49
.= 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 set ; :: 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 Th47;

now

let vv be Vector of (VectQuot V,(LKer f)); :: thesis:
thus (QForm f) . vv,w = (RQForm (LQForm f)) . vv,ww by Th49
.= 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 set ; :: 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 Th48;

now

let ww be Vector of (VectQuot W,(RKer f)); :: thesis:
thus (LQForm (RQForm f)) . v,ww = (QForm f) . vv,ww by Th49
.= 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 set ; :: 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 Th48;

now

let ww be Vector of (VectQuot W,(RKer f)); :: thesis:
thus (QForm f) . v,ww = (LQForm (RQForm f)) . vv,ww by Th49
.= 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 set ; :: 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

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

end;

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

end;

let x be set ; :: 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

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

end;

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