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

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 ;

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 (LQForm f) or x in rightker f )
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 ;

end;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

hence
x in rightker (LQForm f)
by A1; :: thesis: verumlet 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;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

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

hence
x in rightker f
by A4; :: thesis: verumlet 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;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