set K = F_Complex ;
let V, W be VectSp of F_Complex ; :: thesis: for f being sesquilinear-Form of V,W holds
( leftker (Q*Form f) = leftker (RQ*Form (LQForm f)) & rightker (Q*Form f) = rightker (RQ*Form (LQForm f)) & leftker (Q*Form f) = leftker (LQForm (RQ*Form f)) & rightker (Q*Form f) = rightker (LQForm (RQ*Form f)) )
let f be sesquilinear-Form of V,W; :: thesis: ( leftker (Q*Form f) = leftker (RQ*Form (LQForm f)) & rightker (Q*Form f) = rightker (RQ*Form (LQForm f)) & leftker (Q*Form f) = leftker (LQForm (RQ*Form f)) & rightker (Q*Form f) = rightker (LQForm (RQ*Form f)) )
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: ( leftker (RQ*Form (LQForm f)) c= leftker (Q*Form f) & rightker (Q*Form f) = rightker (RQ*Form (LQForm f)) & leftker (Q*Form f) = leftker (LQForm (RQ*Form f)) & rightker (Q*Form f) = rightker (LQForm (RQ*Form f)) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (Q*Form f) or x in leftker (RQ*Form (LQForm f)) )
assume x in leftker (Q*Form f) ; :: thesis: x in leftker (RQ*Form (LQForm f))
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

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

end;

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (RQ*Form (LQForm f)) or x in leftker (Q*Form f) )
assume x in leftker (RQ*Form (LQForm f)) ; :: thesis: x in leftker (Q*Form f)
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

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

end;

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (Q*Form f) or x in rightker (RQ*Form (LQForm f)) )
assume x in rightker (Q*Form f) ; :: thesis: x in rightker (RQ*Form (LQForm f))
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 Th64;

now

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

end;

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (RQ*Form (LQForm f)) or x in rightker (Q*Form f) )
assume x in rightker (RQ*Form (LQForm f)) ; :: thesis: x in rightker (Q*Form f)
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 Th64;

now

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

end;

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (Q*Form f) or x in leftker (LQForm (RQ*Form f)) )
assume x in leftker (Q*Form f) ; :: thesis: x in leftker (LQForm (RQ*Form f))
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 Th65;

now

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

end;

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (LQForm (RQ*Form f)) or x in leftker (Q*Form f) )
assume x in leftker (LQForm (RQ*Form f)) ; :: thesis: x in leftker (Q*Form f)
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 Th65;

now

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

end;

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (Q*Form f) or x in rightker (LQForm (RQ*Form f)) )
assume x in rightker (Q*Form f) ; :: thesis: x in rightker (LQForm (RQ*Form f))
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

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

end;

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (LQForm (RQ*Form f)) or x in rightker (Q*Form f) )
assume x in rightker (LQForm (RQ*Form f)) ; :: thesis: x in rightker (Q*Form f)
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

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

end;

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