let V, W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex ; 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; 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; 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; 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; 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 BILINEAR:28
.=
((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
; verum