let V, W be Z_Module; :: thesis: for v being Vector of V
for w, t being Vector of W
for f being additiveFAF homogeneousFAF FrForm of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let v be Vector of V; :: thesis: for w, t being Vector of W
for f being additiveFAF homogeneousFAF FrForm of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let y, z be Vector of W; :: thesis: for f being additiveFAF homogeneousFAF FrForm of V,W holds f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))
let f be additiveFAF homogeneousFAF FrForm of V,W; :: thesis: f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))
thus f . (v,(y - z)) = (f . (v,y)) + (f . (v,(- z))) by HTh27
.= (f . (v,y)) + (f . (v,((- (1. INT.Ring)) * z))) by VECTSP_1:14
.= (f . (v,y)) + ((- (1. INT.Ring)) * (f . (v,z))) by HTh32
.= (f . (v,y)) - (f . (v,z)) ; :: thesis: verum