set K = F_Complex ;
let V, W be VectSp of F_Complex ; :: thesis: for v being Vector of V
for w, t being Vector of W
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let v1 be Vector of V; :: thesis: for w, t being Vector of W
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds f . (v1,(w - t)) = (f . (v1,w)) - (f . (v1,t))
let w, w2 be Vector of W; :: thesis: for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds f . (v1,(w - w2)) = (f . (v1,w)) - (f . (v1,w2))
let f be additiveFAF cmplxhomogeneousFAF Form of V,W; :: thesis: f . (v1,(w - w2)) = (f . (v1,w)) - (f . (v1,w2))
thus f . (v1,(w - w2)) = (f . (v1,w)) + (f . (v1,(- w2))) by BILINEAR:27
.= (f . (v1,w)) + (f . (v1,((- (1_ F_Complex)) * w2))) by VECTSP_1:14
.= (f . (v1,w)) + (((- (1. F_Complex)) *') * (f . (v1,w2))) by Th27
.= (f . (v1,w)) + ((- (1_ F_Complex)) * (f . (v1,w2))) by COMPLFLD:49, COMPLFLD:52
.= (f . (v1,w)) - (f . (v1,w2)) by VECTSP_6:48 ; :: thesis: verum