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

for f being Functional of V

for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))

let V, W be non empty ModuleStr over K; :: thesis: for f being Functional of V

for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))

let f be Functional of V; :: thesis: for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))

let g be Functional of W; :: thesis: ker g c= rightker (FormFunctional (f,g))

set fg = FormFunctional (f,g);

A1: ker g = { w where w is Vector of W : g . w = 0. K } by VECTSP10:def 9;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ker g or x in rightker (FormFunctional (f,g)) )

assume x in ker g ; :: thesis: x in rightker (FormFunctional (f,g))

then consider w being Vector of W such that

A2: x = w and

A3: g . w = 0. K by A1;

for f being Functional of V

for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))

let V, W be non empty ModuleStr over K; :: thesis: for f being Functional of V

for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))

let f be Functional of V; :: thesis: for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))

let g be Functional of W; :: thesis: ker g c= rightker (FormFunctional (f,g))

set fg = FormFunctional (f,g);

A1: ker g = { w where w is Vector of W : g . w = 0. K } by VECTSP10:def 9;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ker g or x in rightker (FormFunctional (f,g)) )

assume x in ker g ; :: thesis: x in rightker (FormFunctional (f,g))

then consider w being Vector of W such that

A2: x = w and

A3: g . w = 0. K by A1;

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

hence
x in rightker (FormFunctional (f,g))
by A2; :: thesis: verumlet v be Vector of V; :: thesis: (FormFunctional (f,g)) . (v,w) = 0. K

thus (FormFunctional (f,g)) . (v,w) = (f . v) * (g . w) by Def10

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

end;thus (FormFunctional (f,g)) . (v,w) = (f . v) * (g . w) by Def10

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