let K be non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for V, W being non empty ModuleStr over 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 ModuleStr over 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 object ; :: 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 :: thesis: for v being Vector of V holds f . v = (0Functional V) . v

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

end;

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

end;

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