let K be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for V, W being non empty VectSpStr of 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 VectSpStr of 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 set ; :: 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

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 Def11
.= 0. K by A3, VECTSP_1:39 ; :: thesis: verum

end;

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