let V be RealLinearSpace; :: thesis: for M being convex Subset of V
for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let M be convex Subset of V; :: thesis: for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let N be Subset of V; :: thesis: for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let L be Linear_Combination of N; :: thesis: ( L is convex & N c= M implies Sum L in M )
assume that
A1: L is convex and
A2: N c= M ; :: thesis: Sum L in M
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one and
A4: rng F = Carrier L and
A5: 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 ) ) ) by A1, CONVEX1:def 3;
consider f being FinSequence of REAL such that
A6: len f = len F and
A7: Sum f = 1 and
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A5;
A9: len F >= 1

proof

Carrier L <> {} by A1, CONVEX1:21;
then not Carrier L, {} are_equipotent by CARD_1:46;
then card (Carrier L) <> card {} by CARD_1:21;
then len F <> card {} by A3, A4, FINSEQ_4:77;
then len F > 0 by CARD_1:47;
then len F >= 0 + 1 by NAT_1:13;
hence len F >= 1 ; :: thesis: verum

end;

then reconsider i = len F as non empty Element of NAT ;
defpred S₁[ Nat] means (1 / (Sum (mid f,1,$1))) * (Sum (mid (L (#) F),1,$1)) in M;
A10: len (L (#) F) = len F by RLVECT_2:def 9;
A11: S₁[1]

proof

mid f,1,1 = f | 1 by JORDAN3:25;
then A12: len (mid f,1,1) = 1 by A6, A9, FINSEQ_1:80;
then 1 in dom (mid f,1,1) by FINSEQ_3:27;
then reconsider m = (mid f,1,1) . 1 as Element of REAL by PARTFUN1:27;
mid f,1,1 = <*((mid f,1,1) . 1)*> by A12, FINSEQ_1:57;
then A13: Sum (mid f,1,1) = m by FINSOP_1:12;
mid (L (#) F),1,1 = (L (#) F) | 1 by JORDAN3:25;
then A14: len (mid (L (#) F),1,1) = 1 by A9, A10, FINSEQ_1:80;
1 in Seg (len (L (#) F)) by A9, A10;
then A15: ( 1 in dom (L (#) F) & 1 in dom F & 1 in dom f ) by A6, A10, FINSEQ_1:def 3;
then A16: F /. 1 = F . 1 by PARTFUN1:def 8;
A17: (mid (L (#) F),1,1) . 1 = (L (#) F) . 1 by A9, A10, JORDAN3:32
.= (L . (F /. 1)) * (F /. 1) by A15, RLVECT_2:def 9 ;
f . 1 = L . (F . 1) by A8, A15
.= L . (F /. 1) by A15, PARTFUN1:def 8 ;
then A18: Sum (mid f,1,1) = L . (F /. 1) by A6, A9, A13, JORDAN3:32;
A19: F . 1 in rng F by A15, FUNCT_1:def 5;
then F . 1 in { v where v is Element of V : L . v <> 0 } by A4, RLVECT_2:def 6;
then consider v2 being Element of V such that
A20: ( F . 1 = v2 & L . v2 <> 0 ) ;
mid (L (#) F),1,1 = <*((mid (L (#) F),1,1) . 1)*> by A14, FINSEQ_1:57;
then A21: (1 / (Sum (mid f,1,1))) * (Sum (mid (L (#) F),1,1)) = (1 / (Sum (mid f,1,1))) * ((L . (F /. 1)) * (F /. 1)) by A17, RLVECT_1:61
.= ((1 / (Sum (mid f,1,1))) * (L . (F /. 1))) * (F /. 1) by RLVECT_1:def 9
.= 1 * (F /. 1) by A16, A18, A20, XCMPLX_1:107
.= F /. 1 by RLVECT_1:def 9 ;
Carrier L c= N by RLVECT_2:def 8;
then Carrier L c= M by A2, XBOOLE_1:1;
hence S₁[1] by A4, A16, A19, A21; :: thesis: verum

end;

A22: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non empty Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A23: (1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k)) in M ; :: thesis: S₁[k + 1]
A24: k >= 1 by NAT_1:14;

now

per cases ( k >= len f or k < len f ) ;

suppose A25: k >= len f ; :: thesis: S₁[k + 1]

A26: mid f,1,k = f | k by JORDAN3:25, NAT_1:14
.= f by A25, FINSEQ_1:79 ;
A27: mid (L (#) F),1,k = (L (#) F) | k by JORDAN3:25, NAT_1:14
.= L (#) F by A6, A10, A25, FINSEQ_1:79 ;
A28: mid f,1,(k + 1) = f | (k + 1) by JORDAN3:25, NAT_1:12
.= f by A25, FINSEQ_1:79, NAT_1:12 ;
mid (L (#) F),1,(k + 1) = (L (#) F) | (k + 1) by JORDAN3:25, NAT_1:12
.= L (#) F by A6, A10, A25, FINSEQ_1:79, NAT_1:12 ;
hence S₁[k + 1] by A23, A26, A27, A28; :: thesis: verum

end;

suppose A29: k < len f ; :: thesis: S₁[k + 1]

then A30: ( k + 1 >= 1 & k + 1 <= len f ) by NAT_1:13, NAT_1:14;
mid f,1,k = f | k by JORDAN3:25, NAT_1:14;
then A31: len (mid f,1,k) = k by A29, FINSEQ_1:80;
A32: len <*((mid f,1,(k + 1)) . (k + 1))*> = 1 by FINSEQ_1:57;
mid f,1,(k + 1) = f | (k + 1) by A30, JORDAN3:25;
then len (mid f,1,(k + 1)) = k + 1 by A30, FINSEQ_1:80;
then A33: dom (mid f,1,(k + 1)) = Seg ((len (mid f,1,k)) + (len <*((mid f,1,(k + 1)) . (k + 1))*>)) by A31, A32, FINSEQ_1:def 3;
A34: mid f,1,(k + 1) = f | (k + 1) by A30, JORDAN3:25;
A35: len (f | (k + 1)) = k + 1 by A30, FINSEQ_1:80;
A36: for i being Nat st i in dom (mid f,1,k) holds
(mid f,1,(k + 1)) . i = (mid f,1,k) . i

proof

let i be Nat; :: thesis: ( i in dom (mid f,1,k) implies (mid f,1,(k + 1)) . i = (mid f,1,k) . i )
A37: i in NAT by ORDINAL1:def 13;
assume A38: i in dom (mid f,1,k) ; :: thesis: (mid f,1,(k + 1)) . i = (mid f,1,k) . i
A39: mid f,1,k = f | k by JORDAN3:25, NAT_1:14;
then (f | k) . i = (f | k) /. i by A38, PARTFUN1:def 8;
then A40: (mid f,1,k) . i = f /. i by A38, A39, FINSEQ_4:85;
A41: i in Seg (len (f | k)) by A38, A39, FINSEQ_1:def 3;
len (f | k) = k by A29, FINSEQ_1:80;
then ( 1 <= i & i <= k ) by A41, FINSEQ_1:3;
then ( 1 <= i & i <= k + 1 ) by NAT_1:12;
then i in Seg (k + 1) by A37;
then A42: i in dom (f | (k + 1)) by A35, FINSEQ_1:def 3;
then (f | (k + 1)) . i = (f | (k + 1)) /. i by PARTFUN1:def 8;
hence (mid f,1,(k + 1)) . i = (mid f,1,k) . i by A34, A40, A42, FINSEQ_4:85; :: thesis: verum

end;

for i being Nat st i in dom <*((mid f,1,(k + 1)) . (k + 1))*> holds
(mid f,1,(k + 1)) . ((len (mid f,1,k)) + i) = <*((mid f,1,(k + 1)) . (k + 1))*> . i

proof

let i be Nat; :: thesis: ( i in dom <*((mid f,1,(k + 1)) . (k + 1))*> implies (mid f,1,(k + 1)) . ((len (mid f,1,k)) + i) = <*((mid f,1,(k + 1)) . (k + 1))*> . i )
assume i in dom <*((mid f,1,(k + 1)) . (k + 1))*> ; :: thesis: (mid f,1,(k + 1)) . ((len (mid f,1,k)) + i) = <*((mid f,1,(k + 1)) . (k + 1))*> . i
then i in Seg 1 by FINSEQ_1:55;
then i = 1 by FINSEQ_1:4, TARSKI:def 1;
hence (mid f,1,(k + 1)) . ((len (mid f,1,k)) + i) = <*((mid f,1,(k + 1)) . (k + 1))*> . i by A31, FINSEQ_1:57; :: thesis: verum

end;

then A43: mid f,1,(k + 1) = (mid f,1,k) ^ <*((mid f,1,(k + 1)) . (k + 1))*> by A33, A36, FINSEQ_1:def 7;
k + 1 in Seg (k + 1) by A30;
then A44: k + 1 in dom (f | (k + 1)) by A35, FINSEQ_1:def 3;
then (f | (k + 1)) /. (k + 1) = f /. (k + 1) by FINSEQ_4:85;
then A45: (mid f,1,(k + 1)) . (k + 1) = f /. (k + 1) by A34, A44, PARTFUN1:def 8;
A46: k + 1 in Seg (len f) by A30;
then A47: k + 1 in dom f by FINSEQ_1:def 3;
then A48: (mid f,1,(k + 1)) . (k + 1) = f . (k + 1) by A45, PARTFUN1:def 8
.= L . (F . (k + 1)) by A8, A47 ;
k + 1 in dom F by A6, A46, FINSEQ_1:def 3;
then (mid f,1,(k + 1)) . (k + 1) = L . (F /. (k + 1)) by A48, PARTFUN1:def 8;
then A49: Sum (mid f,1,(k + 1)) = (Sum (mid f,1,k)) + (L . (F /. (k + 1))) by A43, RVSUM_1:104;
A50: k < len (L (#) F) by A6, A29, RLVECT_2:def 9;
then A51: ( k + 1 >= 1 & k + 1 <= len (L (#) F) ) by NAT_1:13, NAT_1:14;
mid (L (#) F),1,k = (L (#) F) | k by JORDAN3:25, NAT_1:14;
then A52: len (mid (L (#) F),1,k) = k by A50, FINSEQ_1:80;
A53: len <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> = 1 by FINSEQ_1:57;
A54: mid (L (#) F),1,(k + 1) = (L (#) F) | (k + 1) by A51, JORDAN3:25;
then len (mid (L (#) F),1,(k + 1)) = k + 1 by A51, FINSEQ_1:80;
then A55: dom (mid (L (#) F),1,(k + 1)) = Seg ((len (mid (L (#) F),1,k)) + (len <*((mid (L (#) F),1,(k + 1)) . (k + 1))*>)) by A52, A53, FINSEQ_1:def 3;
A56: len ((L (#) F) | (k + 1)) = k + 1 by A51, FINSEQ_1:80;
A57: for i being Nat st i in dom (mid (L (#) F),1,k) holds
(mid (L (#) F),1,(k + 1)) . i = (mid (L (#) F),1,k) . i

proof

let i be Nat; :: thesis: ( i in dom (mid (L (#) F),1,k) implies (mid (L (#) F),1,(k + 1)) . i = (mid (L (#) F),1,k) . i )
A58: i in NAT by ORDINAL1:def 13;
assume A59: i in dom (mid (L (#) F),1,k) ; :: thesis: (mid (L (#) F),1,(k + 1)) . i = (mid (L (#) F),1,k) . i
A60: mid (L (#) F),1,k = (L (#) F) | k by JORDAN3:25, NAT_1:14;
then ((L (#) F) | k) . i = ((L (#) F) | k) /. i by A59, PARTFUN1:def 8;
then A61: (mid (L (#) F),1,k) . i = (L (#) F) /. i by A59, A60, FINSEQ_4:85;
A62: i in Seg (len ((L (#) F) | k)) by A59, A60, FINSEQ_1:def 3;
len ((L (#) F) | k) = k by A50, FINSEQ_1:80;
then ( 1 <= i & i <= k ) by A62, FINSEQ_1:3;
then ( 1 <= i & i <= k + 1 ) by NAT_1:12;
then i in Seg (k + 1) by A58;
then A63: i in dom ((L (#) F) | (k + 1)) by A56, FINSEQ_1:def 3;
then ((L (#) F) | (k + 1)) . i = ((L (#) F) | (k + 1)) /. i by PARTFUN1:def 8;
hence (mid (L (#) F),1,(k + 1)) . i = (mid (L (#) F),1,k) . i by A54, A61, A63, FINSEQ_4:85; :: thesis: verum

end;

for i being Nat st i in dom <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> holds
(mid (L (#) F),1,(k + 1)) . ((len (mid (L (#) F),1,k)) + i) = <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> . i

proof

let i be Nat; :: thesis: ( i in dom <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> implies (mid (L (#) F),1,(k + 1)) . ((len (mid (L (#) F),1,k)) + i) = <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> . i )
assume i in dom <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> ; :: thesis: (mid (L (#) F),1,(k + 1)) . ((len (mid (L (#) F),1,k)) + i) = <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> . i
then i in Seg 1 by FINSEQ_1:55;
then i = 1 by FINSEQ_1:4, TARSKI:def 1;
hence (mid (L (#) F),1,(k + 1)) . ((len (mid (L (#) F),1,k)) + i) = <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> . i by A52, FINSEQ_1:57; :: thesis: verum

end;

then A64: mid (L (#) F),1,(k + 1) = (mid (L (#) F),1,k) ^ <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> by A55, A57, FINSEQ_1:def 7;
k + 1 in Seg (k + 1) by A30;
then A65: k + 1 in dom ((L (#) F) | (k + 1)) by A56, FINSEQ_1:def 3;
then ((L (#) F) | (k + 1)) /. (k + 1) = (L (#) F) /. (k + 1) by FINSEQ_4:85;
then A66: (mid (L (#) F),1,(k + 1)) . (k + 1) = (L (#) F) /. (k + 1) by A54, A65, PARTFUN1:def 8;
k + 1 <= len (L (#) F) by A6, A30, RLVECT_2:def 9;
then A67: k + 1 in dom (L (#) F) by A30, FINSEQ_3:27;
then A68: (mid (L (#) F),1,(k + 1)) . (k + 1) = (L (#) F) . (k + 1) by A66, PARTFUN1:def 8
.= (L . (F /. (k + 1))) * (F /. (k + 1)) by A67, RLVECT_2:def 9 ;
set r1 = Sum (mid f,1,k);
set r2 = L . (F /. (k + 1));
set w1 = Sum (mid (L (#) F),1,k);
set w2 = F /. (k + 1);
A69: for i being Nat st i in dom (mid f,1,k) holds
0 <= (mid f,1,k) . i

proof

let i be Nat; :: thesis: ( i in dom (mid f,1,k) implies 0 <= (mid f,1,k) . i )
assume i in dom (mid f,1,k) ; :: thesis: 0 <= (mid f,1,k) . i
then i in Seg k by A31, FINSEQ_1:def 3;
then A71: ( 1 <= i & i <= k ) by FINSEQ_1:3;
then A72: (mid f,1,k) . i = f . i by A29, JORDAN3:32;
( 1 <= i & i <= len f ) by A29, A71, XXREAL_0:2;
then i in dom f by FINSEQ_3:27;
hence 0 <= (mid f,1,k) . i by A8, A72; :: thesis: verum

end;

ex i being Element of NAT st
( i in dom (mid f,1,k) & 0 < (mid f,1,k) . i )

proof

A73: 1 in Seg (len (mid f,1,k)) by A24, A31;
1 <= len f by A29, NAT_1:14;
then A74: 1 in Seg (len f) ;
then 1 in dom f by FINSEQ_1:def 3;
then A75: ( f . 1 = L . (F . 1) & f . 1 >= 0 ) by A8;
1 in dom F by A6, A74, FINSEQ_1:def 3;
then F . 1 in Carrier L by A4, FUNCT_1:def 5;
then F . 1 in { v where v is Element of V : L . v <> 0 } by RLVECT_2:def 6;
then consider v being Element of V such that
A76: ( v = F . 1 & L . v <> 0 ) ;
take 1 ; :: thesis: ( 1 in dom (mid f,1,k) & 0 < (mid f,1,k) . 1 )
thus ( 1 in dom (mid f,1,k) & 0 < (mid f,1,k) . 1 ) by A24, A29, A73, A75, A76, FINSEQ_1:def 3, JORDAN3:32; :: thesis: verum

end;

then A77: Sum (mid f,1,k) > 0 by A69, RVSUM_1:115;
A78: ( F /. (k + 1) in M & L . (F /. (k + 1)) > 0 )

proof

k + 1 in Seg (len F) by A6, A30;
then A79: k + 1 in dom F by FINSEQ_1:def 3;
then F /. (k + 1) = F . (k + 1) by PARTFUN1:def 8;
then A80: F /. (k + 1) in Carrier L by A4, A79, FUNCT_1:def 5;
Carrier L c= N by RLVECT_2:def 8;
hence F /. (k + 1) in M by A2, A80, TARSKI:def 3; :: thesis: L . (F /. (k + 1)) > 0
F /. (k + 1) in { v where v is Element of V : L . v <> 0 } by A80, RLVECT_2:def 6;
then consider v being Element of V such that
A81: ( v = F /. (k + 1) & L . v <> 0 ) ;
k + 1 in Seg (len f) by A30;
then k + 1 in dom f by FINSEQ_1:def 3;
then ( f . (k + 1) = L . (F . (k + 1)) & f . (k + 1) >= 0 ) by A8;
hence L . (F /. (k + 1)) > 0 by A79, A81, PARTFUN1:def 8; :: thesis: verum

end;

then A82: (Sum (mid f,1,k)) + (L . (F /. (k + 1))) > 0 + 0 by A77, XREAL_1:10;
A83: ( 0 < (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)) & (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)) < 1 )

proof

1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1)))) > 0 by A82, XREAL_1:141;
hence (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)) > 0 by A77, XREAL_1:131; :: thesis: (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)) < 1
A84: (Sum (mid f,1,k)) + (L . (F /. (k + 1))) > Sum (mid f,1,k) by A78, XREAL_1:31;
(1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)) = (Sum (mid f,1,k)) / ((Sum (mid f,1,k)) + (L . (F /. (k + 1)))) by XCMPLX_1:100;
hence (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)) < 1 by A77, A84, XREAL_1:191; :: thesis: verum

end;

A85: (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (L . (F /. (k + 1))) = 1 - ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)))

proof

1 - ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))) = (((Sum (mid f,1,k)) + (L . (F /. (k + 1)))) * (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1)))))) - ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))) by A82, XCMPLX_1:107
.= (((Sum (mid f,1,k)) + (L . (F /. (k + 1)))) - (Sum (mid f,1,k))) * (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) ;
hence (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (L . (F /. (k + 1))) = 1 - ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))) ; :: thesis: verum

end;

(1 / (Sum (mid f,1,(k + 1)))) * (Sum (mid (L (#) F),1,(k + 1))) = (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((Sum (mid (L (#) F),1,k)) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A49, A64, A68, FVSUM_1:87
.= (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((1 * (Sum (mid (L (#) F),1,k))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 9
.= (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((((Sum (mid f,1,k)) * (1 / (Sum (mid f,1,k)))) * (Sum (mid (L (#) F),1,k))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A77, XCMPLX_1:107
.= (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (((Sum (mid f,1,k)) * ((1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 9
.= ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((Sum (mid f,1,k)) * ((1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k))))) + ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 9
.= (((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))) * ((1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k)))) + ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 9
.= (((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))) * ((1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k)))) + (((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (L . (F /. (k + 1)))) * (F /. (k + 1))) by RLVECT_1:def 9 ;
hence S₁[k + 1] by A23, A78, A83, A85, CONVEX1:def 2; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A11, A22);
then A86: (1 / (Sum (mid f,1,i))) * (Sum (mid (L (#) F),1,i)) in M ;
A87: len (L (#) F) = len F by RLVECT_2:def 9;
Sum (mid f,1,(len f)) = 1 by A6, A7, A9, JORDAN3:29;
then (1 / (Sum (mid f,1,(len f)))) * (Sum (mid (L (#) F),1,(len (L (#) F)))) = Sum (mid (L (#) F),1,(len (L (#) F))) by RLVECT_1:def 9
.= Sum (L (#) F) by A9, A87, JORDAN3:29 ;
hence Sum L in M by A3, A4, A6, A86, A87, RLVECT_2:def 10; :: thesis: verum