let K be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for V being non empty VectSpStr of K
for f being additiveFAF additiveSAF alternating Form of V,V
for v, w being Vector of V holds f . v,w = - (f . w,v)
let V be non empty VectSpStr of K; :: thesis: for f being additiveFAF additiveSAF alternating Form of V,V
for v, w being Vector of V holds f . v,w = - (f . w,v)
let f be additiveFAF additiveSAF alternating Form of V,V; :: thesis: for v, w being Vector of V holds f . v,w = - (f . w,v)
let v, w be Vector of V; :: thesis: f . v,w = - (f . w,v)
0. K = f . (v + w),(v + w) by Def27
.= ((f . v,v) + (f . v,w)) + ((f . w,v) + (f . w,w)) by Th29
.= ((0. K) + (f . v,w)) + ((f . w,v) + (f . w,w)) by Def27
.= ((0. K) + (f . v,w)) + ((f . w,v) + (0. K)) by Def27
.= ((0. K) + (f . v,w)) + (f . w,v) by RLVECT_1:def 7
.= (f . v,w) + (f . w,v) by RLVECT_1:10 ;
hence f . v,w = - (f . w,v) by RLVECT_1:19; :: thesis: verum