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 ) ) )

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

( 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
sum L = 1
; :: thesis: ( ex v being VECTOR of V st not 0 <= L . v or L is convex )assume
L is convex
; :: thesis: ( sum L = 1 & ( for v being Element of V holds L . b_{2} >= 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;

hence sum L = 1 by A1, A2, A5, Def3; :: thesis: for v being Element of V holds L . b_{2} >= 0

let v be Element of V; :: thesis: L . b_{1} >= 0

end;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

then
L * F = f
by A4, A7;(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;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

hence sum L = 1 by A1, A2, A5, Def3; :: thesis: for v being Element of V holds L . b

let v be Element of V; :: thesis: L . b

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

end;

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 ) ) ) )

hence
L is convex
; :: thesis: verum( 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;( 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