let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for V being non empty VectSpStr of K
for f being alternating bilinear-Form of V,V holds leftker f = rightker f
let V be non empty VectSpStr of K; :: thesis: for f being alternating bilinear-Form of V,V holds leftker f = rightker f
let f be alternating 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 set ; :: 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 & ( for w being Vector of V holds f . v,w = 0. K ) ) ;

now

let w be Vector of V; :: thesis: f . w,v = 0. K
thus f . w,v = - (f . v,w) by Th59
.= - (0. K) by A1
.= 0. K by RLVECT_1:25 ; :: thesis: verum

end;

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker f or x in leftker f )
assume x in rightker f ; :: thesis: x in leftker f
then consider w being Vector of V such that
A2: ( w = x & ( for v being Vector of V holds f . v,w = 0. K ) ) ;

now

let v be Vector of V; :: thesis: f . w,v = 0. K
thus f . w,v = - (f . v,w) by Th59
.= - (0. K) by A2
.= 0. K by RLVECT_1:25 ; :: thesis: verum

end;

hence x in leftker f by A2; :: thesis: verum