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 Th39
.= ((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