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 alternating bilinear-Form of V,V holds leftker f = rightker f
let V be non empty ModuleStr over 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 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 ;

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

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

end;

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

end;

let x be object ; :: 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
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

let v be Vector of V; :: thesis: f . (w,v) = 0. K
thus f . (w,v) = - (f . (v,w)) by Th58
.= - (0. K) by A4
.= 0. K by RLVECT_1:12 ; :: thesis: verum

end;

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