let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for V being non empty ModuleStr over K

for f being symmetric bilinear-Form of V,V holds leftker f = rightker f

let V be non empty ModuleStr over K; :: thesis: for f being symmetric bilinear-Form of V,V holds leftker f = rightker f

let f be symmetric bilinear-Form of V,V; :: thesis: leftker f = rightker f

thus leftker f c= rightker f :: according to XBOOLE_0:def 10 :: thesis: rightker f c= leftker f

assume x in rightker f ; :: thesis: x in leftker f

then consider w being Vector of V such that

A3: w = x and

A4: for v being Vector of V holds f . (v,w) = 0. K ;

for f being symmetric bilinear-Form of V,V holds leftker f = rightker f

let V be non empty ModuleStr over K; :: thesis: for f being symmetric bilinear-Form of V,V holds leftker f = rightker f

let f be symmetric bilinear-Form of V,V; :: thesis: leftker f = rightker f

thus leftker f c= rightker f :: according to XBOOLE_0:def 10 :: thesis: rightker f c= leftker f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker f or x in leftker f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker f or x in rightker f )

assume x in leftker f ; :: thesis: x in rightker f

then consider v being Vector of V such that

A1: v = x and

A2: for w being Vector of V holds f . (v,w) = 0. K ;

end;assume x in leftker f ; :: thesis: x in rightker f

then consider v being Vector of V such that

A1: v = x and

A2: for w being Vector of V holds f . (v,w) = 0. K ;

now :: thesis: for w being Vector of V holds f . (w,v) = 0. K

hence
x in rightker f
by A1; :: thesis: verumlet w be Vector of V; :: thesis: f . (w,v) = 0. K

thus f . (w,v) = f . (v,w) by Def25

.= 0. K by A2 ; :: thesis: verum

end;thus f . (w,v) = f . (v,w) by Def25

.= 0. K by A2 ; :: thesis: verum

assume x in rightker f ; :: thesis: x in leftker f

then consider w being Vector of V such that

A3: w = x and

A4: for v being Vector of V holds f . (v,w) = 0. K ;

now :: thesis: for v being Vector of V holds f . (w,v) = 0. K

hence
x in leftker f
by A3; :: thesis: verumlet v be Vector of V; :: thesis: f . (w,v) = 0. K

thus f . (w,v) = f . (v,w) by Def25

.= 0. K by A4 ; :: thesis: verum

end;thus f . (w,v) = f . (v,w) by Def25

.= 0. K by A4 ; :: thesis: verum