let V, W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr 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 BILINEAR:29
.= ((f . v1,w) + ((s *' ) * (f . v1,w2))) + ((f . (r * w1),w) + (f . (r * w1),(s * w2))) by Th30
.= ((f . v1,w) + ((s *' ) * (f . v1,w2))) + ((r * (f . w1,w)) + (f . (r * w1),(s * w2))) by BILINEAR:32
.= ((f . v1,w) + ((s *' ) * (f . v1,w2))) + ((r * (f . w1,w)) + (r * (f . w1,(s * w2)))) by BILINEAR:32
.= ((f . v1,w) + ((s *' ) * (f . v1,w2))) + ((r * (f . w1,w)) + (r * ((s *' ) * (f . w1,w2)))) by Th30 ; :: thesis: verum