let V be ComplexLinearSpace; :: thesis: Up ((0). 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 ((0). V) & v in Up ((0). V) holds
(z * u) + ((1r - z) * v) in Up ((0). V)
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & u in Up ((0). V) & v in Up ((0). V) implies (z * u) + ((1r - z) * v) in Up ((0). V) )
assume that
ex r being Real st
( z = r & 0 < r & r < 1 ) and
A1: u in Up ((0). V) and
A2: v in Up ((0). V) ; :: thesis: (z * u) + ((1r - z) * v) in Up ((0). V)
v in {(0. V)} by A2, CLVECT_1:def 9;
then A3: v = 0. V by TARSKI:def 1;
u in {(0. V)} by A1, CLVECT_1:def 9;
then u = 0. V by TARSKI:def 1;
then (z * u) + ((1r - z) * v) = (0. V) + ((1r - z) * (0. V)) by A3, CLVECT_1:1
.= (0. V) + (0. V) by CLVECT_1:1
.= 0. V ;
then (z * u) + ((1r - z) * v) in {(0. V)} by TARSKI:def 1;
hence (z * u) + ((1r - z) * v) in Up ((0). V) by CLVECT_1:def 9; :: thesis: verum