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 B1: ( 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 Function of NAT, the carrier of S such that
B3: ( Sum xseq = Sx . (len xseq) & Sx . 0 = 0. S & ( for j being Element of 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 B1;
hence ||.(Sum xseq).|| <= Sum yseq by B1, B3, RVSUM_1:72; :: thesis: verum

end;

A4: now

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

now

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 A5: ( 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
A6: 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 A9: k in dom (xseq | i) ; :: thesis: (yseq | i) . k = ||.((xseq | i) /. k).||
then A7: ( k in Seg i & k in dom xseq ) by RELAT_1:57;
then A8: yseq . k = ||.(xseq /. k).|| by A5;
xseq /. k = xseq . k by A7, PARTFUN1:def 6;
then xseq /. k = (xseq | i) . k by A7, FUNCT_1:49;
then xseq /. k = (xseq | i) /. k by A9, PARTFUN1:def 6;
hence (yseq | i) . k = ||.((xseq | i) /. k).|| by A7, A8, FUNCT_1:49; :: thesis: verum

end;

C1: dom xseq = Seg (i + 1) by A5, FINSEQ_1:def 3;
then A9: yseq . (i + 1) = ||.(xseq /. (i + 1)).|| by A5, FINSEQ_1:4;
A10: 1 <= i + 1 by NAT_1:11;
yseq = (yseq | i) ^ <*(yseq /. (i + 1))*> by A5, FINSEQ_5:21;
then yseq = (yseq | i) ^ <*(yseq . (i + 1))*> by A5, A10, FINSEQ_4:15;
then A11: Sum yseq = (Sum (yseq | i)) + (yseq . (i + 1)) by RVSUM_1:74;
B1: len xseq in dom xseq by C1, A5, FINSEQ_1:4;
then reconsider v = xseq . (len xseq) as Element of S by PARTFUN1:4;
B2: v = xseq /. (i + 1) by A5, B1, PARTFUN1:def 6;
A12: i = len (xseq | i) by A5, FINSEQ_1:59, NAT_1:11;
then xseq | i = xseq | (dom (xseq | i)) by FINSEQ_1:def 3;
then A13: Sum xseq = (Sum (xseq | i)) + v by A5, A12, RLVECT_1:38;
A14: ||.((Sum (xseq | i)) + v).|| <= ||.(Sum (xseq | i)).|| + ||.v.|| by NORMSP_1:def 1;
len (xseq | i) = len (yseq | i) by A5, A12, FINSEQ_1:59, NAT_1:11;
then ||.(Sum (xseq | i)).|| <= Sum (yseq | i) by A4, A6, A12;
then ||.(Sum (xseq | i)).|| + ||.v.|| <= (Sum (yseq | i)) + (yseq . (i + 1)) by A9, B2, XREAL_1:6;
hence ||.(Sum xseq).|| <= Sum yseq by A11, A13, A14, XXREAL_0:2; :: thesis: verum

end;

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

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A3, A4);
hence ||.(Sum xseq).|| <= Sum yseq by A1, A2; :: thesis: verum