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 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 12
.= (f . v,y) + (f . v,(- z)) by Th28
.= (f . v,y) + (f . v,((- (1. K)) * z)) by VECTSP_1:59
.= (f . v,y) + ((- (1. K)) * (f . v,z)) by Th33
.= (f . v,y) + (- ((1. K) * (f . v,z))) by VECTSP_1:41
.= (f . v,y) - ((1. K) * (f . v,z)) by RLVECT_1:def 12
.= (f . v,y) - (f . v,z) by VECTSP_1:def 19 ; :: thesis: verum