let K be ZeroStr ; :: thesis: for V being non empty ModuleStr over K

for f being Form of V,V holds

( leftker f c= diagker f & rightker f c= diagker f )

let V be non empty ModuleStr over K; :: thesis: for f being Form of V,V holds

( leftker f c= diagker f & rightker f c= diagker f )

let f be Form of V,V; :: thesis: ( leftker f c= diagker f & rightker f c= diagker f )

thus leftker f c= diagker f :: thesis: rightker f c= diagker f

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

then consider v being Vector of V such that

A3: v = x and

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

f . (v,v) = 0. K by A4;

hence x in diagker f by A3; :: thesis: verum

for f being Form of V,V holds

( leftker f c= diagker f & rightker f c= diagker f )

let V be non empty ModuleStr over K; :: thesis: for f being Form of V,V holds

( leftker f c= diagker f & rightker f c= diagker f )

let f be Form of V,V; :: thesis: ( leftker f c= diagker f & rightker f c= diagker f )

thus leftker f c= diagker f :: thesis: rightker f c= diagker f

proof

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

assume x in leftker f ; :: thesis: x in diagker 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 ;

f . (v,v) = 0. K by A2;

hence x in diagker f by A1; :: thesis: verum

end;assume x in leftker f ; :: thesis: x in diagker 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 ;

f . (v,v) = 0. K by A2;

hence x in diagker f by A1; :: thesis: verum

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

then consider v being Vector of V such that

A3: v = x and

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

f . (v,v) = 0. K by A4;

hence x in diagker f by A3; :: thesis: verum