let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of K
for W being non empty ModuleStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
let V be VectSp of K; :: thesis: for W being non empty ModuleStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
let W be non empty ModuleStr over K; :: thesis: for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
let f be additiveSAF homogeneousSAF Form of V,W; :: thesis: rightker f = rightker (LQForm f)
set lf = LQForm f;
set qv = VectQuot (V,(LKer f));
thus rightker f c= rightker (LQForm f) :: according to XBOOLE_0:def 10 :: thesis: rightker (LQForm f) c= rightker f

proof

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

now :: thesis: for A being Vector of (VectQuot (V,(LKer f))) holds (LQForm f) . (A,w) = 0. K

let A be Vector of (VectQuot (V,(LKer f))); :: thesis: (LQForm f) . (A,w) = 0. K
consider v being Vector of V such that
A3: A = v + (LKer f) by VECTSP10:22;
thus (LQForm f) . (A,w) = f . (v,w) by A3, Def20
.= 0. K by A2 ; :: thesis: verum

end;

hence x in rightker (LQForm f) by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (LQForm f) or x in rightker f )
assume x in rightker (LQForm f) ; :: thesis: x in rightker f
then consider w being Vector of W such that
A4: x = w and
A5: for A being Vector of (VectQuot (V,(LKer f))) holds (LQForm f) . (A,w) = 0. K ;

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

let v be Vector of V; :: thesis: f . (v,w) = 0. K
reconsider A = v + (LKer f) as Vector of (VectQuot (V,(LKer f))) by VECTSP10:23;
thus f . (v,w) = (LQForm f) . (A,w) by Def20
.= 0. K by A5 ; :: thesis: verum

end;

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