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:35
.= ((f . (v1,w)) - (f . (v1,w2))) - (f . (w1,(w - w2))) by Th35
.= ((f . (v1,w)) - (f . (v1,w2))) - ((f . (w1,w)) - (f . (w1,w2))) by Th35 ; :: thesis: verum