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

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