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