let Y be RealNormSpace; for xseq being FinSequence of Y
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Point of Y st
( v = xseq /. i & yseq . i = ||.v.|| ) ) holds
||.(Sum xseq).|| <= Sum yseq
defpred S1[ Nat] means for xseq being FinSequence of Y
for yseq being FinSequence of REAL st $1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Point of Y st
( v = xseq /. i & yseq . i = ||.v.|| ) ) holds
||.(Sum xseq).|| <= Sum yseq;
A1:
S1[ 0 ]
A3:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume A4:
S1[
i]
;
S1[i + 1]now for xseq being FinSequence of Y
for yseq being FinSequence of REAL st i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Point of Y st
( v = xseq /. i & yseq . i = ||.v.|| ) ) holds
||.(Sum xseq).|| <= Sum yseqlet xseq be
FinSequence of
Y;
for yseq being FinSequence of REAL st i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Point of Y st
( v = xseq /. i & yseq . i = ||.v.|| ) ) holds
||.(Sum xseq).|| <= Sum yseqlet yseq be
FinSequence of
REAL ;
( i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Point of Y st
( v = xseq /. i & yseq . i = ||.v.|| ) ) implies ||.(Sum xseq).|| <= Sum yseq )set xseq0 =
xseq | i;
set yseq0 =
yseq | i;
assume A5:
(
i + 1
= len xseq &
len xseq = len yseq & ( for
i being
Element of
NAT st
i in dom xseq holds
ex
v being
Point of
Y st
(
v = xseq /. i &
yseq . i = ||.v.|| ) ) )
;
||.(Sum xseq).|| <= Sum yseqA6:
for
k being
Element of
NAT st
k in dom (xseq | i) holds
ex
v being
Point of
Y st
(
v = (xseq | i) /. k &
(yseq | i) . k = ||.v.|| )
dom xseq = Seg (i + 1)
by A5, FINSEQ_1:def 3;
then consider w being
Point of
Y such that A10:
(
w = xseq /. (i + 1) &
yseq . (i + 1) = ||.w.|| )
by A5, FINSEQ_1:4;
A11:
( 1
<= i + 1 &
i + 1
<= len yseq )
by A5, NAT_1:11;
yseq = (yseq | i) ^ <*(yseq /. (i + 1))*>
by A5, FINSEQ_5:21;
then
yseq = (yseq | i) ^ <*(yseq . (i + 1))*>
by A11, FINSEQ_4:15;
then A12:
Sum yseq = (Sum (yseq | i)) + (yseq . (i + 1))
by RVSUM_1:74;
A13:
i = len (xseq | i)
by A5, FINSEQ_1:59, NAT_1:11;
then A14:
ex
v being
Point of
Y st
(
v = xseq /. (len xseq) &
Sum xseq = (Sum (xseq | i)) + v )
by A5, Lm2;
A15:
||.((Sum (xseq | i)) + w).|| <= ||.(Sum (xseq | i)).|| + ||.w.||
by NORMSP_1:def 1;
len (xseq | i) = len (yseq | i)
by A5, A13, FINSEQ_1:59, NAT_1:11;
then
||.(Sum (xseq | i)).|| + ||.w.|| <= (Sum (yseq | i)) + (yseq . (i + 1))
by A10, XREAL_1:6, A4, A6, A13;
hence
||.(Sum xseq).|| <= Sum yseq
by A5, A10, A12, A14, A15, XXREAL_0:2;
verum end; hence
S1[
i + 1]
;
verum end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A3);
hence
for xseq being FinSequence of Y
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Point of Y st
( v = xseq /. i & yseq . i = ||.v.|| ) ) holds
||.(Sum xseq).|| <= Sum yseq
; verum