let V, W be VectSp of F_Complex ; :: thesis: for v, u being Vector of V
for w, t being Vector of W
for f being sesquilinear-Form of V,W holds f . (v - u),(w - t) = ((f . v,w) - (f . v,t)) - ((f . u,w) - (f . u,t))
let v1, w1 be Vector of V; :: thesis: for w, t being Vector of W
for f being sesquilinear-Form of V,W holds f . (v1 - w1),(w - t) = ((f . v1,w) - (f . v1,t)) - ((f . w1,w) - (f . w1,t))
let w, w2 be Vector of W; :: thesis: for f being sesquilinear-Form of V,W holds f . (v1 - w1),(w - w2) = ((f . v1,w) - (f . v1,w2)) - ((f . w1,w) - (f . w1,w2))
let f be sesquilinear-Form of V,W; :: thesis: f . (v1 - w1),(w - w2) = ((f . v1,w) - (f . v1,w2)) - ((f . w1,w) - (f . w1,w2))
set v3 = f . v1,w;
set v4 = f . v1,w2;
set v5 = f . w1,w;
set v6 = f . w1,w2;
thus f . (v1 - w1),(w - w2) = (f . v1,(w - w2)) - (f . w1,(w - w2)) by BILINEAR:36
.= ((f . v1,w) - (f . v1,w2)) - (f . w1,(w - w2)) by Th38
.= ((f . v1,w) - (f . v1,w2)) - ((f . w1,w) - (f . w1,w2)) by Th38 ; :: thesis: verum