let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds
( L is convex iff ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) ) )
let L be Linear_Combination of V; :: thesis: ( L is convex iff ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) ) )

hereby :: thesis: ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) implies L is convex )

assume L is convex ; :: thesis: ( sum L = 1 & ( for v being Element of V holds L . b₂ >= 0 ) )
then consider F being FinSequence of the carrier of V such that
A1: F is one-to-one and
A2: rng F = Carrier L and
A3: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) ;
consider f being FinSequence of REAL such that
A4: len f = len F and
A5: Sum f = 1 and
A6: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A3;
A7: len (L * F) = len F by FINSEQ_2:33;

now :: thesis: for k being Nat st 1 <= k & k <= len F holds
(L * F) . k = f . k

let k be Nat; :: thesis: ( 1 <= k & k <= len F implies (L * F) . k = f . k )
assume A8: ( 1 <= k & k <= len F ) ; :: thesis: (L * F) . k = f . k
then k in dom f by A4, FINSEQ_3:25;
then A9: f . k = L . (F . k) by A6;
k in dom (L * F) by A7, A8, FINSEQ_3:25;
hence (L * F) . k = f . k by A9, FUNCT_1:12; :: thesis: verum

end;

then L * F = f by A4, A7;
hence sum L = 1 by A1, A2, A5, Def3; :: thesis: for v being Element of V holds L . b₂ >= 0
let v be Element of V; :: thesis: L . b₁ >= 0

per cases ( v in Carrier L or not v in Carrier L ) ;

suppose v in Carrier L ; :: thesis: L . b₁ >= 0

then consider n being object such that
A10: n in dom F and
A11: F . n = v by A2, FUNCT_1:def 3;
A12: dom f = dom F by A4, FINSEQ_3:29;
then f . n = L . (F . n) by A6, A10;
hence L . v >= 0 by A6, A10, A11, A12; :: thesis: verum

end;

suppose not v in Carrier L ; :: thesis: L . b₁ >= 0

hence L . v >= 0 ; :: thesis: verum

end;

end;

end;

assume sum L = 1 ; :: thesis: ( ex v being VECTOR of V st not 0 <= L . v or L is convex )
then consider F being FinSequence of V such that
A13: ( F is one-to-one & rng F = Carrier L ) and
A14: 1 = Sum (L * F) by Def3;
assume A15: for v being Element of V holds L . v >= 0 ; :: thesis: L is convex

now :: thesis: ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) )

take F = F; :: thesis: ( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) )
thus ( F is one-to-one & rng F = Carrier L ) by A13; :: thesis: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) )
take f = L * F; :: thesis: ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) )
thus ( len f = len F & Sum f = 1 ) by A14, FINSEQ_2:33; :: thesis: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
then A16: dom F = dom f by FINSEQ_3:29;
let n be Nat; :: thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A17: n in dom f ; :: thesis: ( f . n = L . (F . n) & f . n >= 0 )
then A18: f . n = L . (F . n) by FUNCT_1:12;
F . n = F /. n by A16, A17, PARTFUN1:def 6;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A15, A18; :: thesis: verum

end;

hence L is convex ; :: thesis: verum