set K = F_Complex ;
let V be non empty ModuleStr over F_Complex ; :: thesis: for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f = leftker (RQ*Form f)
let W be VectSp of F_Complex ; :: thesis: for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds leftker f = leftker (RQ*Form f)
let f be additiveFAF cmplxhomogeneousFAF Form of V,W; :: thesis: leftker f = leftker (RQ*Form f)
set rf = RQ*Form f;
set qw = VectQuot (W,(RKer (f *')));
thus leftker f c= leftker (RQ*Form f) :: according to XBOOLE_0:def 10 :: thesis: leftker (RQ*Form f) c= leftker f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker f or x in leftker (RQ*Form f) )
assume x in leftker f ; :: thesis: x in leftker (RQ*Form f)
then consider v being Vector of V such that
A1: x = v and
A2: for w being Vector of W holds f . (v,w) = 0. F_Complex ;

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

let A be Vector of (VectQuot (W,(RKer (f *')))); :: thesis: (RQ*Form f) . (v,A) = 0. F_Complex
consider w being Vector of W such that
A3: A = w + (RKer (f *')) by VECTSP10:22;
thus (RQ*Form f) . (v,A) = f . (v,w) by A3, Th59
.= 0. F_Complex by A2 ; :: thesis: verum

end;

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

end;

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

now :: thesis: for w being Vector of W holds f . (v,w) = 0. F_Complex

let w be Vector of W; :: thesis: f . (v,w) = 0. F_Complex
reconsider A = w + (RKer (f *')) as Vector of (VectQuot (W,(RKer (f *')))) by VECTSP10:23;
thus f . (v,w) = (RQ*Form f) . (v,A) by Th59
.= 0. F_Complex by A5 ; :: thesis: verum

end;

hence x in leftker f by A4; :: thesis: verum