let f, g be real-valued FinSequence; :: thesis: ( ( for x being Nat holds
( f . x >= g . x & ex i being Nat st f . (i + 1) > g . (i + 1) ) ) implies Sum f > Sum g )
assume A1: for x being Nat holds
( f . x >= g . x & ex i being Nat st f . (i + 1) > g . (i + 1) ) ; :: thesis: Sum f > Sum g
consider i being Nat such that
A2: f . (i + 1) > g . (i + 1) by A1;
A5: Sum f = ((Sum (f | i)) + (f . (i + 1))) + (Sum (f /^ (i + 1))) by SUM;
A6: Sum g = ((Sum (g | i)) + (g . (i + 1))) + (Sum (g /^ (i + 1))) by SUM;
for x being Nat holds
( (f | i) . x >= (g | i) . x & (f /^ (i + 1)) . x >= (g /^ (i + 1)) . x )

proof

let x be Nat; :: thesis: ( (f | i) . x >= (g | i) . x & (f /^ (i + 1)) . x >= (g /^ (i + 1)) . x )
B0: ( i >= x implies ( (f | i) . x = f . x & (g | i) . x = g . x ) ) by FINSEQ_3:112;
( len (f | i) <= i & len (g | i) <= i ) by FINSEQ_5:17;
then ( i < x implies ( len (f | i) < x & len (g | i) < x ) ) by XXREAL_0:2;
then ( i < x implies ( not x in dom (f | i) & not x in dom (g | i) ) ) by FINSEQ_3:25;
then B2: ( i < x implies ( (f | i) . x = 0 & 0 = (g | i) . x ) ) by FUNCT_1:def 2;
( x <> 0 implies ( f . ((i + 1) + x) = (f /^ (i + 1)) . x & g . ((i + 1) + x) = (g /^ (i + 1)) . x ) ) by FINSEQ74;
hence ( (f | i) . x >= (g | i) . x & (f /^ (i + 1)) . x >= (g /^ (i + 1)) . x ) by A1, B0, B2; :: thesis: verum

end;

then ( Sum (f | i) >= Sum (g | i) & Sum (f /^ (i + 1)) >= Sum (g /^ (i + 1)) ) by NYS;
then (Sum (f | i)) + (Sum (f /^ (i + 1))) >= (Sum (g | i)) + (Sum (g /^ (i + 1))) by XREAL_1:7;
then A7: ((Sum (f | i)) + (Sum (f /^ (i + 1)))) + (f . (i + 1)) >= ((Sum (g | i)) + (Sum (g /^ (i + 1)))) + (f . (i + 1)) by XREAL_1:6;
((Sum (g | i)) + (Sum (g /^ (i + 1)))) + (f . (i + 1)) > ((Sum (g | i)) + (Sum (g /^ (i + 1)))) + (g . (i + 1)) by A2, XREAL_1:6;
hence Sum f > Sum g by A5, A6, A7, XXREAL_0:2; :: thesis: verum