let Y be RealNormSpace; :: thesis: 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 S₁[ 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: S₁[ 0 ]

proof

let xseq be FinSequence of Y; :: thesis: for yseq being FinSequence of REAL st 0 = 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
let yseq be FinSequence of REAL ; :: thesis: ( 0 = 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 )
assume A2: ( 0 = 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.|| ) ) ) ; :: thesis: ||.(Sum xseq).|| <= Sum yseq
then <*> the carrier of Y = xseq ;
then ( Sum xseq = 0. Y & <*> REAL = yseq ) by A2, RLVECT_1:43;
hence ||.(Sum xseq).|| <= Sum yseq by RVSUM_1:72; :: thesis: verum

end;

A3: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]

now :: thesis: 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 yseq

let xseq be FinSequence of Y; :: thesis: 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 yseq
let yseq be FinSequence of REAL ; :: thesis: ( 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.|| ) ) ) ; :: thesis: ||.(Sum xseq).|| <= Sum yseq
A6: 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.|| )

proof

let k be Element of NAT ; :: thesis: ( k in dom (xseq | i) implies ex v being Point of Y st
( v = (xseq | i) /. k & (yseq | i) . k = ||.v.|| ) )
assume A7: k in dom (xseq | i) ; :: thesis: ex v being Point of Y st
( v = (xseq | i) /. k & (yseq | i) . k = ||.v.|| )
then A8: ( k in Seg i & k in dom xseq ) by RELAT_1:57;
then consider v being Point of Y such that
A9: ( v = xseq /. k & yseq . k = ||.v.|| ) by A5;
take v ; :: thesis: ( v = (xseq | i) /. k & (yseq | i) . k = ||.v.|| )
xseq /. k = xseq . k by A8, PARTFUN1:def 6;
then xseq /. k = (xseq | i) . k by A8, FUNCT_1:49;
hence ( v = (xseq | i) /. k & (yseq | i) . k = ||.v.|| ) by A9, A8, A7, PARTFUN1:def 6, FUNCT_1:49; :: thesis: verum

end;

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; :: thesis: verum

end;

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

end;

for i being Nat holds S₁[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 ; :: thesis: verum