let f, g be real-valued FinSequence; :: thesis: ( ( for x being Nat holds f . x >= g . x ) implies Sum f >= Sum g )
assume A0: for x being Nat holds f . x >= g . x ; :: thesis: Sum f >= Sum g
reconsider f = f, g = g as FinSequence of REAL by FINSEQ_1:102;

per cases ( len f <= len g or len f > len g ) ;

suppose len f <= len g ; :: thesis: Sum f >= Sum g

then len f = min ((len f),(len g)) by XXREAL_0:def 9;
then B1: Sum (f | (len f)) >= Sum (g | (len f)) by A0, LmFG;
for r being Real st r in rng (g /^ (len f)) holds
r <= 0

proof

let r be Real; :: thesis: ( r in rng (g /^ (len f)) implies r <= 0 )
assume C1: r in rng (g /^ (len f)) ; :: thesis: r <= 0
consider k being object such that
C2: ( k in dom (g /^ (len f)) & r = (g /^ (len f)) . k ) by C1, FUNCT_1:def 3;
reconsider k = k as non zero Nat by C2, FINSEQ_3:25;
C4: (len f) + k in dom g by C2, FINSEQ_5:26;
r = (g /^ (len f)) /. k by C2, PARTFUN1:def 6
.= g /. ((len f) + k) by C2, FINSEQ_5:27
.= g . ((len f) + k) by PARTFUN1:def 6, C4 ;
then r <= f . ((len f) + k) by A0;
hence r <= 0 ; :: thesis: verum

end;

then reconsider h = g /^ (len f) as nonpositive-yielding FinSequence of REAL by PARTFUN3:def 3;
C5: Sum g = Sum ((g | (len f)) ^ (g /^ (len f))) by RFINSEQ:8
.= (Sum (g | (len f))) + (Sum (g /^ (len f))) by RVSUM_1:75 ;
Sum h <= 0 ;
then (Sum (g | (len f))) + 0 >= (Sum (g | (len f))) + (Sum (g /^ (len f))) by XREAL_1:6;
hence Sum f >= Sum g by B1, C5, XXREAL_0:2; :: thesis: verum

end;

suppose len f > len g ; :: thesis: Sum f >= Sum g

then len g = min ((len f),(len g)) by XXREAL_0:def 9;
then B1: Sum (f | (len g)) >= Sum (g | (len g)) by A0, LmFG;
for r being Real st r in rng (f /^ (len g)) holds
r >= 0

proof

let r be Real; :: thesis: ( r in rng (f /^ (len g)) implies r >= 0 )
assume C1: r in rng (f /^ (len g)) ; :: thesis: r >= 0
consider k being object such that
C2: ( k in dom (f /^ (len g)) & r = (f /^ (len g)) . k ) by C1, FUNCT_1:def 3;
reconsider k = k as non zero Nat by C2, FINSEQ_3:25;
C4: (len g) + k in dom f by C2, FINSEQ_5:26;
r = (f /^ (len g)) /. k by C2, PARTFUN1:def 6
.= f /. ((len g) + k) by C2, FINSEQ_5:27
.= f . ((len g) + k) by PARTFUN1:def 6, C4 ;
then r >= g . ((len g) + k) by A0;
hence r >= 0 ; :: thesis: verum

end;

then reconsider h = f /^ (len g) as nonnegative-yielding FinSequence of REAL by PARTFUN3:def 4;
C5: Sum f = Sum ((f | (len g)) ^ (f /^ (len g))) by RFINSEQ:8
.= (Sum (f | (len g))) + (Sum (f /^ (len g))) by RVSUM_1:75 ;
Sum h >= 0 ;
then (Sum (f | (len g))) + 0 <= (Sum (f | (len g))) + (Sum (f /^ (len g))) by XREAL_1:6;
hence Sum f >= Sum g by B1, C5, XXREAL_0:2; :: thesis: verum

end;

end;