let K be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for V being non empty ModuleStr over 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 ModuleStr over 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 Def26
.= ((f . (v,v)) + (f . (v,w))) + ((f . (w,v)) + (f . (w,w))) by Th28
.= ((0. K) + (f . (v,w))) + ((f . (w,v)) + (f . (w,w))) by Def26
.= ((0. K) + (f . (v,w))) + ((f . (w,v)) + (0. K)) by Def26
.= ((0. K) + (f . (v,w))) + (f . (w,v)) by RLVECT_1:def 4
.= (f . (v,w)) + (f . (w,v)) by RLVECT_1:4 ;
hence f . (v,w) = - (f . (w,v)) by RLVECT_1:6; :: thesis: verum