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 & ( 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 A1 ; :: 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
A2: ( x = vv & ( 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 A2 ; :: thesis:

end;

hence x in leftker (QForm f) by A2; :: 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
A3: ( x = ww & ( 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 A3 ; :: thesis:

end;

hence x in rightker (RQForm (LQForm f)) by A3; :: 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
A4: ( x = ww & ( 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 A4 ; :: thesis:

end;

hence x in rightker (QForm f) by A4; :: 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
A5: ( x = vv & ( 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 A5 ; :: thesis:

end;

hence x in leftker (LQForm (RQForm f)) by A5; :: 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
A6: ( x = vv & ( 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 A6 ; :: thesis:

end;

hence x in leftker (QForm f) by A6; :: 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
A7: ( x = ww & ( 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 A7 ; :: thesis:

end;

hence x in rightker (LQForm (RQForm f)) by A7; :: 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
A8: ( x = ww & ( 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 A8 ; :: thesis:

end;

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