let V, W be VectSp of F_Complex ; :: thesis: for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of F_Complex
for f being sesquilinear-Form of V,W holds f . ((v - (a * u)),(w - (b * t))) = ((f . (v,w)) - ((b *') * (f . (v,t)))) - ((a * (f . (u,w))) - (a * ((b *') * (f . (u,t)))))
let v1, w1 be Vector of V; :: thesis: for w, t being Vector of W
for a, b being Element of F_Complex
for f being sesquilinear-Form of V,W holds f . ((v1 - (a * w1)),(w - (b * t))) = ((f . (v1,w)) - ((b *') * (f . (v1,t)))) - ((a * (f . (w1,w))) - (a * ((b *') * (f . (w1,t)))))
let w, w2 be Vector of W; :: thesis: for a, b being Element of F_Complex
for f being sesquilinear-Form of V,W holds f . ((v1 - (a * w1)),(w - (b * w2))) = ((f . (v1,w)) - ((b *') * (f . (v1,w2)))) - ((a * (f . (w1,w))) - (a * ((b *') * (f . (w1,w2)))))
let r, s be Element of F_Complex; :: thesis: for f being sesquilinear-Form of V,W holds f . ((v1 - (r * w1)),(w - (s * w2))) = ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (r * ((s *') * (f . (w1,w2)))))
let f be sesquilinear-Form of V,W; :: thesis: f . ((v1 - (r * w1)),(w - (s * w2))) = ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (r * ((s *') * (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 - (r * w1)),(w - (s * w2))) = ((f . (v1,w)) - (f . (v1,(s * w2)))) - ((f . ((r * w1),w)) - (f . ((r * w1),(s * w2)))) by Th36
.= ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((f . ((r * w1),w)) - (f . ((r * w1),(s * w2)))) by Th27
.= ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (f . ((r * w1),(s * w2)))) by BILINEAR:31
.= ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (r * (f . (w1,(s * w2))))) by BILINEAR:31
.= ((f . (v1,w)) - ((s *') * (f . (v1,w2)))) - ((r * (f . (w1,w))) - (r * ((s *') * (f . (w1,w2))))) by Th27 ; :: thesis: verum