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)) )

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 ;

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

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

end;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 :: thesis: for ww being Vector of (VectQuot (W,(RKer ((LQForm f) *')))) holds (RQ*Form (LQForm f)) . (vv,ww) = 0. F_Complex

hence
x in leftker (RQ*Form (LQForm f))
by A1; :: thesis: verumlet 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 Th61;

thus (RQ*Form (LQForm f)) . (vv,ww) = (Q*Form f) . (vv,w) by Th63

.= 0. F_Complex by A2 ; :: thesis: verum

end;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: verum

proof

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

end;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 :: thesis: for ww being Vector of (VectQuot (W,(RKer (f *')))) holds (Q*Form f) . (vv,ww) = 0. F_Complex

hence
x in leftker (Q*Form f)
by A3; :: thesis: verumlet 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 Th61;

thus (Q*Form f) . (vv,ww) = (RQ*Form (LQForm f)) . (vv,w) by Th63

.= 0. F_Complex by A4 ; :: thesis: verum

end;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: verum

proof

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)) )
let x be object ; :: 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 Th61;

end;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 Th61;

now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds (RQ*Form (LQForm f)) . (vv,w) = 0. F_Complex

hence
x in rightker (RQ*Form (LQForm f))
by A5; :: thesis: verumlet 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 Th63

.= 0. F_Complex by A6 ; :: thesis: verum

end;thus (RQ*Form (LQForm f)) . (vv,w) = (Q*Form f) . (vv,ww) by Th63

.= 0. F_Complex by A6 ; :: thesis: verum

proof

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)) )
let x be object ; :: 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 Th61;

end;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 Th61;

now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds (Q*Form f) . (vv,w) = 0. F_Complex

hence
x in rightker (Q*Form f)
by A7; :: thesis: verumlet 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 Th63

.= 0. F_Complex by A8 ; :: thesis: verum

end;thus (Q*Form f) . (vv,w) = (RQ*Form (LQForm f)) . (vv,ww) by Th63

.= 0. F_Complex by A8 ; :: thesis: verum

proof

thus
leftker (LQForm (RQ*Form f)) c= leftker (Q*Form f)
:: thesis: rightker (Q*Form f) = rightker (LQForm (RQ*Form f))
let x be object ; :: 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 Th62;

end;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 Th62;

now :: thesis: for ww being Vector of (VectQuot (W,(RKer (f *')))) holds (LQForm (RQ*Form f)) . (v,ww) = 0. F_Complex

hence
x in leftker (LQForm (RQ*Form f))
by A9; :: thesis: verumlet 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 Th63

.= 0. F_Complex by A10 ; :: thesis: verum

end;thus (LQForm (RQ*Form f)) . (v,ww) = (Q*Form f) . (vv,ww) by Th63

.= 0. F_Complex by A10 ; :: thesis: verum

proof

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)
let x be object ; :: 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 Th62;

end;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 Th62;

now :: thesis: for ww being Vector of (VectQuot (W,(RKer (f *')))) holds (Q*Form f) . (v,ww) = 0. F_Complex

hence
x in leftker (Q*Form f)
by A11; :: thesis: verumlet 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 Th63

.= 0. F_Complex by A12 ; :: thesis: verum

end;thus (Q*Form f) . (v,ww) = (LQForm (RQ*Form f)) . (vv,ww) by Th63

.= 0. F_Complex by A12 ; :: thesis: verum

proof

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

end;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 :: thesis: for vv being Vector of (VectQuot (V,(LKer (RQ*Form f)))) holds (LQForm (RQ*Form f)) . (vv,ww) = 0. F_Complex

hence
x in rightker (LQForm (RQ*Form f))
by A13; :: thesis: verumlet 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 Th62;

thus (LQForm (RQ*Form f)) . (vv,ww) = (Q*Form f) . (v,ww) by Th63

.= 0. F_Complex by A14 ; :: thesis: verum

end;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: verum

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 :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds (Q*Form f) . (vv,ww) = 0. F_Complex

hence
x in rightker (Q*Form f)
by A15; :: thesis: verumlet 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 Th62;

thus (Q*Form f) . (vv,ww) = (LQForm (RQ*Form f)) . (v,ww) by Th63

.= 0. F_Complex by A16 ; :: thesis: verum

end;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: verum