let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V being non empty VectSpStr of K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
let V be non empty VectSpStr of K; :: thesis: for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
let W be VectSp of K; :: thesis: for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
let f be additiveFAF homogeneousFAF Form of V,W; :: thesis: leftker f = leftker (RQForm f)
set rf = RQForm f;
set qw = VectQuot W,(RKer f);
thus leftker f c= leftker (RQForm f) :: according to XBOOLE_0:def 10 :: thesis: leftker (RQForm f) c= leftker f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker f or x in leftker (RQForm f) )
assume x in leftker f ; :: thesis: x in leftker (RQForm 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. K ;

now

let A be Vector of (VectQuot W,(RKer f)); :: thesis: (RQForm f) . v,A = 0. K
consider w being Vector of W such that
A3: A = w + (RKer f) by VECTSP10:23;
thus (RQForm f) . v,A = f . v,w by A3, Def22
.= 0. K by A2 ; :: thesis: verum

end;

hence x in leftker (RQForm f) by A1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (RQForm f) or x in leftker f )
assume x in leftker (RQForm 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 (RQForm f) . v,A = 0. K ;

now

let w be Vector of W; :: thesis: f . v,w = 0. K
reconsider A = w + (RKer f) as Vector of (VectQuot W,(RKer f)) by VECTSP10:24;
thus f . v,w = (RQForm f) . v,A by Def22
.= 0. K by A5 ; :: thesis: verum

end;

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