let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V holds leftker (ScalarForm f) = leftker (Q*Form f)
let f be diagReR+0valued hermitan-Form of V; :: thesis: leftker (ScalarForm f) = leftker (Q*Form f)
set vq = VectQuot V,(LKer f);
set vr = VectQuot V,(RKer (f *' ));
set qf = Q*Form f;
set qhf = ScalarForm f;
set K = F_Complex ;
thus leftker (ScalarForm f) c= leftker (Q*Form f) :: according to XBOOLE_0:def 10 :: thesis: leftker (Q*Form f) c= leftker (ScalarForm f)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (ScalarForm f) or x in leftker (Q*Form f) )
assume x in leftker (ScalarForm f) ; :: thesis: x in leftker (Q*Form f)
then consider A being Vector of (VectQuot V,(LKer f)) such that
A1: ( x = A & ( for B being Vector of (VectQuot V,(LKer f)) holds (ScalarForm f) . A,B = 0. F_Complex ) ) ;

now

let B be Vector of (VectQuot V,(RKer (f *' ))); :: thesis: (Q*Form f) . A,B = 0. F_Complex
reconsider w = B as Vector of (VectQuot V,(LKer f)) by Th59;
thus (Q*Form f) . A,B = (ScalarForm f) . A,w
.= 0. F_Complex by A1 ; :: thesis: verum

end;

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (Q*Form f) or x in leftker (ScalarForm f) )
assume x in leftker (Q*Form f) ; :: thesis: x in leftker (ScalarForm f)
then consider A being Vector of (VectQuot V,(LKer f)) such that
A2: ( x = A & ( for B being Vector of (VectQuot V,(RKer (f *' ))) holds (Q*Form f) . A,B = 0. F_Complex ) ) ;

now

let B be Vector of (VectQuot V,(LKer f)); :: thesis: (ScalarForm f) . A,B = 0. F_Complex
reconsider w = B as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
thus (ScalarForm f) . A,B = (Q*Form f) . A,w
.= 0. F_Complex by A2 ; :: thesis: verum

end;

hence x in leftker (ScalarForm f) by A2; :: thesis: verum