thus ( f is alternating implies for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) ) by Th59; :: thesis: ( ( for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) ) implies f is alternating )
assume A1: for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) ; :: thesis: f is alternating
let v be Vector of V; :: according to BILINEAR:def 27 :: thesis: f . (v,v) = 0. K
f . (v,v) = - (f . (v,v)) by A1;
then (f . (v,v)) + (f . (v,v)) = 0. K by VECTSP_1:63;
hence f . (v,v) = 0. K by VECTSP_1:def 30; :: thesis: verum