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 additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed

let V, W be non empty ModuleStr over K; :: thesis: for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed

let f be additiveFAF homogeneousFAF Form of V,W; :: thesis: rightker f is linearly-closed

set V1 = rightker f;

thus for v, u being Vector of W st v in rightker f & u in rightker f holds

v + u in rightker 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 W holds

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

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

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

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

then consider v1 being Vector of W such that

A7: v1 = v and

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

for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed

let V, W be non empty ModuleStr over K; :: thesis: for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed

let f be additiveFAF homogeneousFAF Form of V,W; :: thesis: rightker f is linearly-closed

set V1 = rightker f;

thus for v, u being Vector of W st v in rightker f & u in rightker f holds

v + u in rightker 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 W; :: thesis: ( v in rightker f & u in rightker f implies v + u in rightker f )

assume that

A1: v in rightker f and

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

consider u1 being Vector of W such that

A3: u1 = u and

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

consider v1 being Vector of W such that

A5: v1 = v and

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

end;assume that

A1: v in rightker f and

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

consider u1 being Vector of W such that

A3: u1 = u and

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

consider v1 being Vector of W such that

A5: v1 = v and

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

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

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

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

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

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

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

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

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

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

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

( not b

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

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

then consider v1 being Vector of W such that

A7: v1 = v and

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

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

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

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

.= a * (0. K) by A8

.= 0. K ; :: thesis: verum

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

.= a * (0. K) by A8

.= 0. K ; :: thesis: verum