let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V being VectSp of K
for W being non empty VectSpStr of 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 VectSpStr of K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
let W be non empty VectSpStr of 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 set ; :: 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 & ( for v being Vector of V holds f . v,w = 0. K ) ) ;

now

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

end;

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

end;

let x be set ; :: 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
A3: ( x = w & ( for A being Vector of (VectQuot V,(LKer f)) holds (LQForm f) . A,w = 0. K ) ) ;

now

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:24;
thus f . v,w = (LQForm f) . A,w by Def21
.= 0. K by A3 ; :: thesis: verum

end;

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