let m be Element of NAT ; :: thesis: for xseq being FinSequence of REAL m
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 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 Element of 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 Element of 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 Element of 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 Element of 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:10, RVSUM_1:102; :: thesis: verum

end;

A3: 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 REAL m; :: 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 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 Element of 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 A5: ( i + 1 = len xseq & len xseq = len yseq & ( for i being Element of 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
A6: for k being Element of 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 Element of 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 A7: ( k in Seg i & k in dom xseq ) by RELAT_1:86;
then consider v being Element of REAL m such that
A8: ( v = xseq . k & yseq . k = |.v.| ) by A5;
take v ; :: thesis: ( v = (xseq | i) . k & (yseq | i) . k = |.v.| )
thus ( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) by A7, A8, FUNCT_1:72; :: thesis: verum

end;

dom xseq = Seg (i + 1) by A5, FINSEQ_1:def 3;
then consider w being Element of REAL m such that
A9: ( w = xseq . (i + 1) & yseq . (i + 1) = |.w.| ) by A5, FINSEQ_1:6;
A10: ( 1 <= i + 1 & i + 1 <= len yseq ) by A5, NAT_1:11;
yseq = (yseq | i) ^ <*(yseq /. (i + 1))*> by A5, FINSEQ_5:24;
then yseq = (yseq | i) ^ <*(yseq . (i + 1))*> by A10, FINSEQ_4:24;
then A11: Sum yseq = (Sum (yseq | i)) + (yseq . (i + 1)) by RVSUM_1:104;
A12: i = len (xseq | i) by A5, FINSEQ_1:80, NAT_1:11;
then A13: ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A5, LOPBTh2581;
A14: |.((Sum (xseq | i)) + w).| <= |.(Sum (xseq | i)).| + |.w.| by EUCLID:15;
len (xseq | i) = len (yseq | i) by A5, A12, FINSEQ_1:80, NAT_1:11;
then |.(Sum (xseq | i)).| <= Sum (yseq | i) by A4, A6, A12;
then |.(Sum (xseq | i)).| + |.w.| <= (Sum (yseq | i)) + (yseq . (i + 1)) by A9, XREAL_1:8;
hence |.(Sum xseq).| <= Sum yseq by A5, A9, 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(A1, A3);
hence for xseq being FinSequence of REAL m
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 Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq ; :: thesis: verum