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

proof

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;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker f or x in 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