let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V, W being VectSp of K
for v, u being Vector of V
for w being Vector of W
for f being additiveSAF homogeneousSAF Form of V,W holds f . (v - u),w = (f . v,w) - (f . u,w)
let V, W be VectSp of K; :: thesis: for v, u being Vector of V
for w being Vector of W
for f being additiveSAF homogeneousSAF Form of V,W holds f . (v - u),w = (f . v,w) - (f . u,w)
let v, w be Vector of V; :: thesis: for w being Vector of W
for f being additiveSAF homogeneousSAF Form of V,W holds f . (v - w),w = (f . v,w) - (f . w,w)
let y be Vector of W; :: thesis: for f being additiveSAF homogeneousSAF Form of V,W holds f . (v - w),y = (f . v,y) - (f . w,y)
let f be additiveSAF homogeneousSAF Form of V,W; :: thesis: f . (v - w),y = (f . v,y) - (f . w,y)
thus f . (v - w),y = f . (v + (- w)),y by RLVECT_1:def 12
.= (f . v,y) + (f . (- w),y) by Th27
.= (f . v,y) + (f . ((- (1. K)) * w),y) by VECTSP_1:59
.= (f . v,y) + ((- (1. K)) * (f . w,y)) by Th32
.= (f . v,y) + (- ((1. K) * (f . w,y))) by VECTSP_1:41
.= (f . v,y) - ((1. K) * (f . w,y)) by RLVECT_1:def 12
.= (f . v,y) - (f . w,y) by VECTSP_1:def 19 ; :: thesis: verum