for V, W being 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)))))