let V, W be Z_Module; :: 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,y)) + (f . ((- w),y)) by BLTh26
.= (f . (v,y)) + (f . (((- (1. INT.Ring)) * w),y)) by ZMODUL01:2
.= (f . (v,y)) + ((- (1. INT.Ring)) * (f . (w,y))) by BLTh31
.= (f . (v,y)) - (f . (w,y)) ; :: thesis: verum