let S be RealNormSpace; :: thesis: for xseq being FinSequence of S
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = ||.(xseq /. i).|| ) holds
||.(Sum xseq).|| <= Sum yseq
let xseq be FinSequence of S; :: thesis: for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = ||.(xseq /. i).|| ) holds
||.(Sum xseq).|| <= Sum yseq
let yseq be FinSequence of REAL ; :: thesis: ( len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = ||.(xseq /. i).|| ) implies ||.(Sum xseq).|| <= Sum yseq )
assume that
A1: len xseq = len yseq and
A2: for i being Element of NAT st i in dom xseq holds
yseq . i = ||.(xseq /. i).|| ; :: thesis: ||.(Sum xseq).|| <= Sum yseq
defpred S₁[ Nat] means for xseq being FinSequence of S
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
yseq . i = ||.(xseq /. i).|| ) holds
||.(Sum xseq).|| <= Sum yseq;
A3: S₁[ 0 ]

proof

let xseq be FinSequence of S; :: 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
yseq . i = ||.(xseq /. i).|| ) 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
yseq . i = ||.(xseq /. i).|| ) implies ||.(Sum xseq).|| <= Sum yseq )
assume A4: ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = ||.(xseq /. i).|| ) ) ; :: thesis: ||.(Sum xseq).|| <= Sum yseq
consider Sx being sequence of the carrier of S such that
A5: ( Sum xseq = Sx . (len xseq) & Sx . 0 = 0. S & ( for j being Nat
for v being Element of S st j < len xseq & v = xseq . (j + 1) holds
Sx . (j + 1) = (Sx . j) + v ) ) by RLVECT_1:def 12;
yseq = {} by A4;
hence ||.(Sum xseq).|| <= Sum yseq by A4, A5, RVSUM_1:72; :: thesis: verum

end;

A6: 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 A7: S₁[i] ; :: thesis: S₁[i + 1]

now :: thesis: for xseq being FinSequence of S
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
yseq . i = ||.(xseq /. i).|| ) holds
||.(Sum xseq).|| <= Sum yseq

let xseq be FinSequence of S; :: 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
yseq . i = ||.(xseq /. i).|| ) 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
yseq . i = ||.(xseq /. i).|| ) implies ||.(Sum xseq).|| <= Sum yseq )
set xseq0 = xseq | i;
set yseq0 = yseq | i;
assume A8: ( i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = ||.(xseq /. i).|| ) ) ; :: thesis: ||.(Sum xseq).|| <= Sum yseq
A9: for k being Element of NAT st k in dom (xseq | i) holds
(yseq | i) . k = ||.((xseq | i) /. k).||

proof

let k be Element of NAT ; :: thesis: ( k in dom (xseq | i) implies (yseq | i) . k = ||.((xseq | i) /. k).|| )
assume A10: k in dom (xseq | i) ; :: thesis: (yseq | i) . k = ||.((xseq | i) /. k).||
then A11: ( k in Seg i & k in dom xseq ) by RELAT_1:57;
then A12: yseq . k = ||.(xseq /. k).|| by A8;
xseq /. k = xseq . k by A11, PARTFUN1:def 6;
then xseq /. k = (xseq | i) . k by A11, FUNCT_1:49;
then xseq /. k = (xseq | i) /. k by A10, PARTFUN1:def 6;
hence (yseq | i) . k = ||.((xseq | i) /. k).|| by A11, A12, FUNCT_1:49; :: thesis: verum

end;

A13: dom xseq = Seg (i + 1) by A8, FINSEQ_1:def 3;
then A14: yseq . (i + 1) = ||.(xseq /. (i + 1)).|| by A8, FINSEQ_1:4;
A15: 1 <= i + 1 by NAT_1:11;
yseq = (yseq | i) ^ <*(yseq /. (i + 1))*> by A8, FINSEQ_5:21;
then yseq = (yseq | i) ^ <*(yseq . (i + 1))*> by A8, A15, FINSEQ_4:15;
then A16: Sum yseq = (Sum (yseq | i)) + (yseq . (i + 1)) by RVSUM_1:74;
reconsider v = xseq . (len xseq) as Element of S by A13, A8, FINSEQ_1:4, PARTFUN1:4;
A18: v = xseq /. (i + 1) by A8, A13, FINSEQ_1:4, PARTFUN1:def 6;
A19: i = len (xseq | i) by A8, FINSEQ_1:59, NAT_1:11;
then xseq | i = xseq | (dom (xseq | i)) by FINSEQ_1:def 3;
then A20: Sum xseq = (Sum (xseq | i)) + v by A8, A19, RLVECT_1:38;
A21: ||.((Sum (xseq | i)) + v).|| <= ||.(Sum (xseq | i)).|| + ||.v.|| by NORMSP_1:def 1;
len (xseq | i) = len (yseq | i) by A8, A19, FINSEQ_1:59, NAT_1:11;
then ||.(Sum (xseq | i)).|| + ||.v.|| <= (Sum (yseq | i)) + (yseq . (i + 1)) by A7, A9, A19, A14, A18, XREAL_1:6;
hence ||.(Sum xseq).|| <= Sum yseq by A16, A20, A21, 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(A3, A6);
hence ||.(Sum xseq).|| <= Sum yseq by A1, A2; :: thesis: verum