let K be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for f being Functional of V
for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional f,g) = ker g
let V, W be non empty VectSpStr of K; :: thesis: for f being Functional of V
for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional f,g) = ker g
let f be Functional of V; :: thesis: for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional f,g) = ker g
let g be Functional of W; :: thesis: ( f <> 0Functional V implies rightker (FormFunctional f,g) = ker g )
set fg = FormFunctional f,g;
assume A1: f <> 0Functional V ; :: thesis: rightker (FormFunctional f,g) = ker g
A2: ker g = { w where w is Vector of W : g . w = 0. K } by VECTSP10:def 9;
thus rightker (FormFunctional f,g) c= ker g :: according to XBOOLE_0:def 10 :: thesis: ker g c= rightker (FormFunctional f,g)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (FormFunctional f,g) or x in ker g )
assume x in rightker (FormFunctional f,g) ; :: thesis: x in ker g
then consider w being Vector of W such that
A3: x = w and
A4: for v being Vector of V holds (FormFunctional f,g) . v,w = 0. K ;
assume not x in ker g ; :: thesis: contradiction
then A5: g . w <> 0. K by A2, A3;

now

let v be Vector of V; :: thesis: f . v = (0Functional V) . v
(f . v) * (g . w) = (FormFunctional f,g) . v,w by Def11
.= 0. K by A4 ;
hence f . v = 0. K by A5, VECTSP_1:44
.= (0Functional V) . v by HAHNBAN1:22 ;
:: thesis: verum

end;

hence contradiction by A1, FUNCT_2:113; :: thesis: verum

end;

thus ker g c= rightker (FormFunctional f,g) by Th53; :: thesis: verum