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 f c= leftker (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 f c= leftker (FormFunctional (f,g))
let f be Functional of V; :: thesis: for g being Functional of W holds ker f c= leftker (FormFunctional (f,g))
let g be Functional of W; :: thesis: ker f c= leftker (FormFunctional (f,g))
set fg = FormFunctional (f,g);
A1: ker f = { v where v is Vector of V : f . v = 0. K } by VECTSP10:def 9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ker f or x in leftker (FormFunctional (f,g)) )
assume x in ker f ; :: thesis: x in leftker (FormFunctional (f,g))
then consider v being Vector of V such that
A2: x = v and
A3: f . v = 0. K by A1;

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

let w be Vector of W; :: 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;

hence x in leftker (FormFunctional (f,g)) by A2; :: thesis: verum