let m be Nat; :: thesis: for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq
defpred S₁[ Nat] means for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st $1 = len xseq & len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq;
A1: S₁[ 0 ]

proof

let xseq be FinSequence of REAL m; :: thesis: for yseq being FinSequence of REAL st 0 = len xseq & len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m 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 Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) implies |.(Sum xseq).| <= Sum yseq )
assume ( 0 = len xseq & len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) ) ; :: thesis: |.(Sum xseq).| <= Sum yseq
then ( Sum xseq = 0* m & <*> REAL = yseq ) by EUCLID_7:def 11;
hence |.(Sum xseq).| <= Sum yseq by EUCLID:7, RVSUM_1:72; :: thesis: verum

end;

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

now :: thesis: for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st i + 1 = len xseq & len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq

let xseq be FinSequence of REAL m; :: thesis: for yseq being FinSequence of REAL st i + 1 = len xseq & len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m 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 Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) implies |.(Sum xseq).| <= Sum yseq )
set xseq0 = xseq | i;
set yseq0 = yseq | i;
assume A4: ( i + 1 = len xseq & len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) ) ; :: thesis: |.(Sum xseq).| <= Sum yseq
A5: for k being Nat st k in dom (xseq | i) holds
ex v being Element of REAL m st
( v = (xseq | i) . k & (yseq | i) . k = |.v.| )

proof

let k be Nat; :: thesis: ( k in dom (xseq | i) implies ex v being Element of REAL m st
( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) )
assume k in dom (xseq | i) ; :: thesis: ex v being Element of REAL m st
( v = (xseq | i) . k & (yseq | i) . k = |.v.| )
then A6: ( k in Seg i & k in dom xseq ) by RELAT_1:57;
then consider v being Element of REAL m such that
A7: ( v = xseq . k & yseq . k = |.v.| ) by A4;
take v ; :: thesis: ( v = (xseq | i) . k & (yseq | i) . k = |.v.| )
thus ( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) by A6, A7, FUNCT_1:49; :: thesis: verum

end;

dom xseq = Seg (i + 1) by A4, FINSEQ_1:def 3;
then consider w being Element of REAL m such that
A8: ( w = xseq . (i + 1) & yseq . (i + 1) = |.w.| ) by A4, FINSEQ_1:4;
A9: ( 1 <= i + 1 & i + 1 <= len yseq ) by A4, NAT_1:11;
yseq = (yseq | i) ^ <*(yseq /. (i + 1))*> by A4, FINSEQ_5:21;
then yseq = (yseq | i) ^ <*(yseq . (i + 1))*> by A9, FINSEQ_4:15;
then A10: Sum yseq = (Sum (yseq | i)) + (yseq . (i + 1)) by RVSUM_1:74;
A11: i = len (xseq | i) by A4, FINSEQ_1:59, NAT_1:11;
then A12: ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A4, Th15;
A13: |.((Sum (xseq | i)) + w).| <= |.(Sum (xseq | i)).| + |.w.| by EUCLID:12;
len (xseq | i) = len (yseq | i) by A4, A11, FINSEQ_1:59, NAT_1:11;
then |.(Sum (xseq | i)).| <= Sum (yseq | i) by A3, A5, A11;
then |.(Sum (xseq | i)).| + |.w.| <= (Sum (yseq | i)) + (yseq . (i + 1)) by A8, XREAL_1:6;
hence |.(Sum xseq).| <= Sum yseq by A4, A8, A10, A12, A13, 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, A2);
hence for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq ; :: thesis: verum