thus
( f is alternating implies for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) )
by Th58; :: 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 26 :: 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:16;

hence f . (v,v) = 0. K by VECTSP_1:def 18; :: thesis: verum

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 26 :: 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:16;

hence f . (v,v) = 0. K by VECTSP_1:def 18; :: thesis: verum