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