let V be ComplexLinearSpace; :: thesis: Up ((Omega). V) is convex
let u, v be VECTOR of V; :: according to CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in Up ((Omega). V) & v in Up ((Omega). V) holds
(z * u) + ((1r - z) * v) in Up ((Omega). V)
thus for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in Up ((Omega). V) & v in Up ((Omega). V) holds
(z * u) + ((1r - z) * v) in Up ((Omega). V) ; :: thesis: verum