let f be FinSequence of NAT ; :: thesis: for i, j being Nat st i in dom f & j in dom f & i <> j holds
Sum f >= (f . i) + (f . j)
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i <> j implies Sum f >= (f . i) + (f . j) )
assume AS: ( i in dom f & j in dom f & i <> j ) ; :: thesis: Sum f >= (f . i) + (f . j)
then A: f <> {} ;

now :: thesis: not len f = 1

assume len f = 1 ; :: thesis: contradiction
then B: dom f = {1} by FINSEQ_1:def 3, FINSEQ_1:2;
then i = 1 by AS, TARSKI:def 1
.= j by AS, B, TARSKI:def 1 ;
hence contradiction by AS; :: thesis: verum

end;

then B: len f >= 2 by A, NAT_1:23;
defpred S₁[ Nat] means for f being FinSequence of NAT
for i being Nat st i in dom f & j in dom f & i <> j & len f = $1 holds
Sum f >= (f . i) + (f . j);
IA: S₁[2]

proof

now :: thesis: for f being FinSequence of NAT
for i being Nat st i in dom f & j in dom f & i <> j & len f = 2 holds
Sum f >= (f . i) + (f . j)

let f be FinSequence of NAT ; :: thesis: for i being Nat st i in dom f & j in dom f & i <> j & len f = 2 holds
Sum b₂ >= (b₂ . b₃) + (b₂ . j)
let i be Nat; :: thesis: ( i in dom f & j in dom f & i <> j & len f = 2 implies Sum b₁ >= (b₁ . b₂) + (b₁ . j) )
assume A1: ( i in dom f & j in dom f & i <> j & len f = 2 ) ; :: thesis: Sum b₁ >= (b₁ . b₂) + (b₁ . j)
then ( f . i = f /. i & f . j = f /. j ) by PARTFUN1:def 6;
then reconsider ni = f . i, nj = f . j as Element of NAT ;
A0: dom f = {1,2} by A1, FINSEQ_1:def 3, FINSEQ_1:2;

per cases then ( i = 1 or i = 2 ) by A1, TARSKI:def 2;

suppose A2: i = 1 ; :: thesis: Sum b₁ >= (b₁ . b₂) + (b₁ . j)

then nj = f . 2 by A1, A0, TARSKI:def 2;
then Sum f = Sum <*ni,nj*> by A1, A2, FINSEQ_1:44
.= ni + nj by RVSUM_1:77 ;
hence Sum f >= (f . i) + (f . j) ; :: thesis: verum

end;

suppose A2: i = 2 ; :: thesis: Sum b₁ >= (b₁ . b₂) + (b₁ . j)

then nj = f . 1 by A1, A0, TARSKI:def 2;
then Sum f = Sum <*nj,ni*> by A1, A2, FINSEQ_1:44
.= nj + ni by RVSUM_1:77 ;
hence Sum f >= (f . i) + (f . j) ; :: thesis: verum

end;

end;

end;

hence S₁[2] ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st 2 <= k & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( 2 <= k & S₁[k] implies S₁[k + 1] )
assume 2 <= k ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume I2: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f being FinSequence of NAT
for i being Nat st i in dom f & j in dom f & i <> j & len f = k + 1 holds
Sum f >= (f . i) + (f . j)

let f be FinSequence of NAT ; :: thesis: for i being Nat st i in dom f & j in dom f & i <> j & len f = k + 1 holds
Sum b₂ >= (b₂ . b₃) + (b₂ . j)
let i be Nat; :: thesis: ( i in dom f & j in dom f & i <> j & len f = k + 1 implies Sum b₁ >= (b₁ . b₂) + (b₁ . j) )
assume I3: ( i in dom f & j in dom f & i <> j & len f = k + 1 ) ; :: thesis: Sum b₁ >= (b₁ . b₂) + (b₁ . j)
then consider g being FinSequence of NAT , d being Element of NAT such that
I4: f = g ^ <*d*> by FINSEQ_2:19;
I5: len f = (len g) + 1 by I4, FINSEQ_2:16;
then I7: dom g = Seg k by I3, FINSEQ_1:def 3;
I6: Sum f = (Sum g) + d by I4, RVSUM_1:74;
dom f = Seg (k + 1) by I3, FINSEQ_1:def 3;
then I8: ( 1 <= i & i <= k + 1 & 1 <= j & j <= k + 1 ) by I3, FINSEQ_1:1;

per cases then ( i = k + 1 or j = k + 1 or ( i < k + 1 & j < k + 1 ) ) by XXREAL_0:1;

suppose J1: i = k + 1 ; :: thesis: Sum b₁ >= (b₁ . b₂) + (b₁ . j)

then J2: f . i = d by I3, I4, I5, FINSEQ_1:42;
j < k + 1 by J1, I3, I8, XXREAL_0:1;
then j <= k by NAT_1:13;
then H: j in dom g by I7, I8, FINSEQ_1:1;
Sum g >= g . j by NEWTON04:21;
then Sum g >= f . j by I4, H, FINSEQ_1:def 7;
hence Sum f >= (f . i) + (f . j) by I6, J2, XREAL_1:6; :: thesis: verum

end;

suppose J1: j = k + 1 ; :: thesis: Sum b₁ >= (b₁ . b₂) + (b₁ . j)

then J2: f . j = d by I3, I4, I5, FINSEQ_1:42;
i < k + 1 by J1, I3, I8, XXREAL_0:1;
then i <= k by NAT_1:13;
then H: i in dom g by I7, I8, FINSEQ_1:1;
Sum g >= g . i by NEWTON04:21;
then Sum g >= f . i by I4, H, FINSEQ_1:def 7;
hence Sum f >= (f . i) + (f . j) by I6, J2, XREAL_1:6; :: thesis: verum

end;

suppose ( i < k + 1 & j < k + 1 ) ; :: thesis: Sum b₁ >= (b₁ . b₂) + (b₁ . j)

then ( i <= k & j <= k ) by NAT_1:13;
then H: ( i in dom g & j in dom g ) by I7, I8, FINSEQ_1:1;
then Sum g >= (g . i) + (g . j) by I2, I5, I3;
then Sum g >= (f . i) + (g . j) by I4, H, FINSEQ_1:def 7;
then Sum g >= (f . i) + (f . j) by I4, H, FINSEQ_1:def 7;
then (Sum g) + d >= ((f . i) + (f . j)) + 0 by XREAL_1:7;
hence Sum f >= (f . i) + (f . j) by I4, RVSUM_1:74; :: thesis: verum

end;

end;

end;

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

end;

for k being Nat st 2 <= k holds
S₁[k] from NAT_1:sch 8(IA, IS);
hence Sum f >= (f . i) + (f . j) by AS, B; :: thesis: verum