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 g c= rightker (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 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 set ; :: 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 & g . w = 0. K ) by A1;

now

let v be Vector of V; :: thesis: (FormFunctional f,g) . v,w = 0. K
thus (FormFunctional f,g) . v,w = (f . v) * (g . w) by Def11
.= 0. K by A2, VECTSP_1:36 ; :: thesis: verum

end;

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