let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 11

.= (f . (v,y)) + (f . ((- w),y)) by Th26

.= (f . (v,y)) + (f . (((- (1. K)) * w),y)) by VECTSP_1:14

.= (f . (v,y)) + ((- (1. K)) * (f . (w,y))) by Th31

.= (f . (v,y)) + (- ((1. K) * (f . (w,y)))) by VECTSP_1:9

.= (f . (v,y)) - ((1. K) * (f . (w,y))) by RLVECT_1:def 11

.= (f . (v,y)) - (f . (w,y)) ; :: thesis: verum

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 11

.= (f . (v,y)) + (f . ((- w),y)) by Th26

.= (f . (v,y)) + (f . (((- (1. K)) * w),y)) by VECTSP_1:14

.= (f . (v,y)) + ((- (1. K)) * (f . (w,y))) by Th31

.= (f . (v,y)) + (- ((1. K) * (f . (w,y)))) by VECTSP_1:9

.= (f . (v,y)) - ((1. K) * (f . (w,y))) by RLVECT_1:def 11

.= (f . (v,y)) - (f . (w,y)) ; :: thesis: verum