begin
Lm1:
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V holds 1 * M = M
Lm2:
for V being RealLinearSpace
for M being non empty Subset of V holds 0 * M = {(0. V)}
Lm3:
for V being non empty add-associative addLoopStr
for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3)
Lm4:
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M
Lm5:
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2)
Lm6:
for V being non empty RLSStruct
for M, N being Subset of V
for r being Real st M c= N holds
r * M c= r * N
Lm7:
for V being non empty RLSStruct
for M being empty Subset of V
for r being Real holds r * M = {}
Lm8:
for V being non empty addLoopStr
for M being empty Subset of V
for N being Subset of V holds M + N = {}
Lm9:
for V being non empty right_zeroed addLoopStr
for M being Subset of V holds M + {(0. V)} = M
Lm10:
for V being RealLinearSpace
for M being Subset of V
for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) c= (r1 + r2) * M
begin
Lm11:
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v} holds
( L . v = 1 & Sum L = (L . v) * v )
Lm12:
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
Lm13:
for p being FinSequence
for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds
p = <*z,y,x*>
Lm14:
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds
Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
Lm15:
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds
( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
begin
begin
theorem
for
p being
FinSequence for
x,
y,
z being
set st
p is
one-to-one &
rng p = {x,y,z} &
x <> y &
y <> z &
z <> x & not
p = <*x,y,z*> & not
p = <*x,z,y*> & not
p = <*y,x,z*> & not
p = <*y,z,x*> & not
p = <*z,x,y*> holds
p = <*z,y,x*> by Lm13;
begin