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))

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

thus
ker g c= rightker (FormFunctional (f,g))
by Th52; :: thesis: verum
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;

end;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

hence
contradiction
by A1, FUNCT_2:63; :: thesis: verumlet 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;(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