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:28
.= (f . v1,w) + (f . v1,((- (1_ F_Complex )) * w2)) by VECTSP_1:59
.= (f . v1,w) + (((- (1. F_Complex )) *' ) * (f . v1,w2)) by Th30
.= (f . v1,w) + ((- (1_ F_Complex )) * (f . v1,w2)) by COMPLFLD:85, COMPLFLD:88
.= (f . v1,w) - (f . v1,w2) by VECTSP_6:81 ; :: thesis: verum