let V be VectSp of F_Complex ; :: thesis:
let f be diagReR+0valued hermitan-Form of V; :: thesis:
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:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in leftker (ScalarForm f) ; :: thesis:
then consider A being Vector of (VectQuot (V,(LKer f))) such that
A1: x = A and
A2: for B being Vector of (VectQuot (V,(LKer f))) holds (ScalarForm f) . (A,B) = 0. F_Complex ;

now :: thesis:

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

end;

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

end;

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

now :: thesis:

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

end;

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