let K be ZeroStr ; :: thesis: for V being non empty VectSpStr of K
for f being Form of V,V holds
( leftker f c= diagker f & rightker f c= diagker f )
let V be non empty VectSpStr of 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 set ; :: 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 & ( for w being Vector of V holds f . v,w = 0. K ) ) ;
f . v,v = 0. K by A1;
hence x in diagker f by A1; :: thesis: verum

end;

let x be set ; :: 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
A2: ( v = x & ( for w being Vector of V holds f . w,v = 0. K ) ) ;
f . v,v = 0. K by A2;
hence x in diagker f by A2; :: thesis: verum