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 being Vector of V

for w, t being Vector of W

for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))

let V, W be VectSp of K; :: thesis: for v being Vector of V

for w, t being Vector of W

for f being additiveFAF homogeneousFAF Form 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 Form 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 Form of V,W holds f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))

let f be additiveFAF homogeneousFAF Form of V,W; :: thesis: f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))

thus f . (v,(y - z)) = f . (v,(y + (- z))) by RLVECT_1:def 11

.= (f . (v,y)) + (f . (v,(- z))) by Th27

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

.= (f . (v,y)) + ((- (1. K)) * (f . (v,z))) by Th32

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

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

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

for v being Vector of V

for w, t being Vector of W

for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))

let V, W be VectSp of K; :: thesis: for v being Vector of V

for w, t being Vector of W

for f being additiveFAF homogeneousFAF Form 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 Form 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 Form of V,W holds f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))

let f be additiveFAF homogeneousFAF Form of V,W; :: thesis: f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))

thus f . (v,(y - z)) = f . (v,(y + (- z))) by RLVECT_1:def 11

.= (f . (v,y)) + (f . (v,(- z))) by Th27

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

.= (f . (v,y)) + ((- (1. K)) * (f . (v,z))) by Th32

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

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

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