let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for V, W being non empty ModuleStr over K

for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed

let V, W be non empty ModuleStr over K; :: thesis: for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed

let f be additiveSAF homogeneousSAF Form of V,W; :: thesis: leftker f is linearly-closed

set V1 = leftker f;

thus for v, u being Vector of V st v in leftker f & u in leftker f holds

v + u in leftker f :: according to VECTSP_4:def 1 :: thesis: for b_{1} being Element of the carrier of K

for b_{2} being Element of the carrier of V holds

( not b_{2} in leftker f or b_{1} * b_{2} in leftker f )_{1} being Element of the carrier of V holds

( not b_{1} in leftker f or a * b_{1} in leftker f )

let v be Vector of V; :: thesis: ( not v in leftker f or a * v in leftker f )

assume v in leftker f ; :: thesis: a * v in leftker f

then consider v1 being Vector of V such that

A7: v1 = v and

A8: for w being Vector of W holds f . (v1,w) = 0. K ;

for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed

let V, W be non empty ModuleStr over K; :: thesis: for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed

let f be additiveSAF homogeneousSAF Form of V,W; :: thesis: leftker f is linearly-closed

set V1 = leftker f;

thus for v, u being Vector of V st v in leftker f & u in leftker f holds

v + u in leftker f :: according to VECTSP_4:def 1 :: thesis: for b

for b

( not b

proof

let a be Element of K; :: thesis: for b
let v, u be Vector of V; :: thesis: ( v in leftker f & u in leftker f implies v + u in leftker f )

assume that

A1: v in leftker f and

A2: u in leftker f ; :: thesis: v + u in leftker f

consider u1 being Vector of V such that

A3: u1 = u and

A4: for w being Vector of W holds f . (u1,w) = 0. K by A2;

consider v1 being Vector of V such that

A5: v1 = v and

A6: for w being Vector of W holds f . (v1,w) = 0. K by A1;

end;assume that

A1: v in leftker f and

A2: u in leftker f ; :: thesis: v + u in leftker f

consider u1 being Vector of V such that

A3: u1 = u and

A4: for w being Vector of W holds f . (u1,w) = 0. K by A2;

consider v1 being Vector of V such that

A5: v1 = v and

A6: for w being Vector of W holds f . (v1,w) = 0. K by A1;

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

hence
v + u in leftker f
; :: thesis: verumlet w be Vector of W; :: thesis: f . ((v + u),w) = 0. K

thus f . ((v + u),w) = (f . (v1,w)) + (f . (u1,w)) by A5, A3, Th26

.= (0. K) + (f . (u1,w)) by A6

.= (0. K) + (0. K) by A4

.= 0. K by RLVECT_1:def 4 ; :: thesis: verum

end;thus f . ((v + u),w) = (f . (v1,w)) + (f . (u1,w)) by A5, A3, Th26

.= (0. K) + (f . (u1,w)) by A6

.= (0. K) + (0. K) by A4

.= 0. K by RLVECT_1:def 4 ; :: thesis: verum

( not b

let v be Vector of V; :: thesis: ( not v in leftker f or a * v in leftker f )

assume v in leftker f ; :: thesis: a * v in leftker f

then consider v1 being Vector of V such that

A7: v1 = v and

A8: for w being Vector of W holds f . (v1,w) = 0. K ;

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

hence
a * v in leftker f
; :: thesis: verumlet w be Vector of W; :: thesis: f . ((a * v),w) = 0. K

thus f . ((a * v),w) = a * (f . (v1,w)) by A7, Th31

.= a * (0. K) by A8

.= 0. K ; :: thesis: verum

end;thus f . ((a * v),w) = a * (f . (v1,w)) by A7, Th31

.= a * (0. K) by A8

.= 0. K ; :: thesis: verum