set K = F_Complex ;
let V, W be VectSp of F_Complex ; :: thesis:
let f be sesquilinear-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 (RQ*Form f)));
set rlf = RQ*Form (LQForm f);
set qf = Q*Form f;
set lrf = LQForm (RQ*Form f);
thus leftker (Q*Form f) c= leftker (RQ*Form (LQForm f)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in leftker (Q*Form 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 (Q*Form f) . (vv,ww) = 0. F_Complex ;

now :: thesis:

let ww be Vector of (VectQuot (W,(RKer ((LQForm f) *')))); :: thesis:
reconsider w = ww as Vector of (VectQuot (W,(RKer (f *')))) by Th61;
thus (RQ*Form (LQForm f)) . (vv,ww) = (Q*Form f) . (vv,w) by Th63
.= 0. F_Complex by A2 ; :: thesis:

end;

hence x in leftker (RQ*Form (LQForm f)) by A1; :: thesis:

end;

thus leftker (RQ*Form (LQForm f)) c= leftker (Q*Form f) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in leftker (RQ*Form (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 (RQ*Form (LQForm f)) . (vv,ww) = 0. F_Complex ;

now :: thesis:

let ww be Vector of (VectQuot (W,(RKer (f *')))); :: thesis:
reconsider w = ww as Vector of (VectQuot (W,(RKer ((LQForm f) *')))) by Th61;
thus (Q*Form f) . (vv,ww) = (RQ*Form (LQForm f)) . (vv,w) by Th63
.= 0. F_Complex by A4 ; :: thesis:

end;

hence x in leftker (Q*Form f) by A3; :: thesis:

end;

thus rightker (Q*Form f) c= rightker (RQ*Form (LQForm f)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rightker (Q*Form 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 (Q*Form f) . (vv,ww) = 0. F_Complex ;
reconsider w = ww as Vector of (VectQuot (W,(RKer ((LQForm f) *')))) by Th61;

now :: thesis:

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis:
thus (RQ*Form (LQForm f)) . (vv,w) = (Q*Form f) . (vv,ww) by Th63
.= 0. F_Complex by A6 ; :: thesis:

end;

hence x in rightker (RQ*Form (LQForm f)) by A5; :: thesis:

end;

thus rightker (RQ*Form (LQForm f)) c= rightker (Q*Form f) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rightker (RQ*Form (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 (RQ*Form (LQForm f)) . (vv,ww) = 0. F_Complex ;
reconsider w = ww as Vector of (VectQuot (W,(RKer (f *')))) by Th61;

now :: thesis:

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis:
thus (Q*Form f) . (vv,w) = (RQ*Form (LQForm f)) . (vv,ww) by Th63
.= 0. F_Complex by A8 ; :: thesis:

end;

hence x in rightker (Q*Form f) by A7; :: thesis:

end;

thus leftker (Q*Form f) c= leftker (LQForm (RQ*Form f)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in leftker (Q*Form 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 (Q*Form f) . (vv,ww) = 0. F_Complex ;
reconsider v = vv as Vector of (VectQuot (V,(LKer (RQ*Form f)))) by Th62;

now :: thesis:

let ww be Vector of (VectQuot (W,(RKer (f *')))); :: thesis:
thus (LQForm (RQ*Form f)) . (v,ww) = (Q*Form f) . (vv,ww) by Th63
.= 0. F_Complex by A10 ; :: thesis:

end;

hence x in leftker (LQForm (RQ*Form f)) by A9; :: thesis:

end;

thus leftker (LQForm (RQ*Form f)) c= leftker (Q*Form f) :: thesis:

proof

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

now :: thesis:

let ww be Vector of (VectQuot (W,(RKer (f *')))); :: thesis:
thus (Q*Form f) . (v,ww) = (LQForm (RQ*Form f)) . (vv,ww) by Th63
.= 0. F_Complex by A12 ; :: thesis:

end;

hence x in leftker (Q*Form f) by A11; :: thesis:

end;

thus rightker (Q*Form f) c= rightker (LQForm (RQ*Form f)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rightker (Q*Form 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 (Q*Form f) . (vv,ww) = 0. F_Complex ;

now :: thesis:

let vv be Vector of (VectQuot (V,(LKer (RQ*Form f)))); :: thesis:
reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th62;
thus (LQForm (RQ*Form f)) . (vv,ww) = (Q*Form f) . (v,ww) by Th63
.= 0. F_Complex by A14 ; :: thesis:

end;

hence x in rightker (LQForm (RQ*Form f)) by A13; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rightker (LQForm (RQ*Form 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 (RQ*Form f)))) holds (LQForm (RQ*Form f)) . (vv,ww) = 0. F_Complex ;

now :: thesis:

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis:
reconsider v = vv as Vector of (VectQuot (V,(LKer (RQ*Form f)))) by Th62;
thus (Q*Form f) . (vv,ww) = (LQForm (RQ*Form f)) . (v,ww) by Th63
.= 0. F_Complex by A16 ; :: thesis:

end;

hence x in rightker (Q*Form f) by A15; :: thesis: