defpred S₁[ Nat] means for xseq, 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 Real st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq;
A1: S₁[ 0 ]

proof

let xseq, 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 Real 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 Real st
( v = xseq . i & yseq . i = |.v.| ) ) ) ; :: thesis: |.(Sum xseq).| <= Sum yseq
then <*> REAL = xseq ;
then ( Sum xseq = 0 & <*> REAL = yseq ) by A2, RVSUM_1:72;
hence |.(Sum xseq).| <= Sum yseq by COMPLEX1:44, 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, 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 Real st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq

let xseq, 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 Real 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 Real 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 Real 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 Real st
( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) )
assume k in dom (xseq | i) ; :: thesis: ex v being Real 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 Real such that
A9: ( 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 A8, A9, FUNCT_1:49; :: thesis: verum

end;

dom xseq = Seg (i + 1) by A5, FINSEQ_1:def 3;
then consider w being Real 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 Real st
( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A5, Lm1;
A15: |.((Sum (xseq | i)) + w).| <= |.(Sum (xseq | i)).| + |.w.| by COMPLEX1:56;
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 A4, A6, A10, A13, XREAL_1:6;
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, 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 Real st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq ; :: thesis: verum