let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being non empty ModuleStr over 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 ModuleStr over 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

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 ;

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 ModuleStr over 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (RQForm f) or x in leftker f )
let x be object ; :: 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 ;

end;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 :: thesis: for A being Vector of (VectQuot (W,(RKer f))) holds (RQForm f) . (v,A) = 0. K

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

thus (RQForm f) . (v,A) = f . (v,w) by A3, Def21

.= 0. K by A2 ; :: thesis: verum

end;consider w being Vector of W such that

A3: A = w + (RKer f) by VECTSP10:22;

thus (RQForm f) . (v,A) = f . (v,w) by A3, Def21

.= 0. K by A2 ; :: thesis: verum

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 :: thesis: for w being Vector of W holds f . (v,w) = 0. K

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

thus f . (v,w) = (RQForm f) . (v,A) by Def21

.= 0. K by A5 ; :: thesis: verum

end;reconsider A = w + (RKer f) as Vector of (VectQuot (W,(RKer f))) by VECTSP10:23;

thus f . (v,w) = (RQForm f) . (v,A) by Def21

.= 0. K by A5 ; :: thesis: verum