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 g <> 0Functional W holds
leftker (FormFunctional f,g) = ker f
let V, W be non empty VectSpStr of K; :: thesis: for f being Functional of V
for g being Functional of W st g <> 0Functional W holds
leftker (FormFunctional f,g) = ker f
let f be Functional of V; :: thesis: for g being Functional of W st g <> 0Functional W holds
leftker (FormFunctional f,g) = ker f
let g be Functional of W; :: thesis: ( g <> 0Functional W implies leftker (FormFunctional f,g) = ker f )
set fg = FormFunctional f,g;
assume A1: g <> 0Functional W ; :: thesis: leftker (FormFunctional f,g) = ker f
A2: ker f = { v where v is Vector of V : f . v = 0. K } by VECTSP10:def 9;
thus leftker (FormFunctional f,g) c= ker f :: according to XBOOLE_0:def 10 :: thesis: ker f c= leftker (FormFunctional f,g)

proof

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

now

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

end;

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

end;

thus ker f c= leftker (FormFunctional f,g) by Th51; :: thesis: verum