let V, W be VectSp of F_Complex ; 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; 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; 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; 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
; verum