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

per cases ( f is empty or g is empty or ( not f is empty & not g is empty ) ) ;

suppose ( f is empty or g is empty ) ; :: thesis: Sum (f | (min ((len f),(len g)))) >= Sum (g | (min ((len f),(len g))))

then min ((len f),(len g)) = 0 by XXREAL_0:def 9;
hence Sum (f | (min ((len f),(len g)))) >= Sum (g | (min ((len f),(len g)))) ; :: thesis: verum

end;

suppose ( not f is empty & not g is empty ) ; :: thesis: Sum (f | (min ((len f),(len g)))) >= Sum (g | (min ((len f),(len g))))

then ( len f >= 1 & len g >= 1 ) by FINSEQ_1:20;
then min ((len f),(len g)) >= 1 by XXREAL_0:def 9;
then A3: ( min ((len f),(len g)) in dom f & min ((len f),(len g)) in dom g ) by XXREAL_0:17, FINSEQ_3:25;
then A4: ( len (f | (min ((len f),(len g)))) = min ((len f),(len g)) & len (g | (min ((len f),(len g)))) = min ((len f),(len g)) ) by NEWTON02:110;
for k being Element of NAT st k in dom (g | (min ((len f),(len g)))) holds
(g | (min ((len f),(len g)))) . k <= (f | (min ((len f),(len g)))) . k

proof

let k be Element of NAT ; :: thesis: ( k in dom (g | (min ((len f),(len g)))) implies (g | (min ((len f),(len g)))) . k <= (f | (min ((len f),(len g)))) . k )
assume k in dom (g | (min ((len f),(len g)))) ; :: thesis: (g | (min ((len f),(len g)))) . k <= (f | (min ((len f),(len g)))) . k
then ( min ((len f),(len g)) >= k & k >= 1 ) by A4, FINSEQ_3:25;
then ( (f | (min ((len f),(len g)))) . k = f . k & (g | (min ((len f),(len g)))) . k = g . k ) by A3, NEWTON02:107;
hence (g | (min ((len f),(len g)))) . k <= (f | (min ((len f),(len g)))) . k by A0; :: thesis: verum

end;

hence Sum (f | (min ((len f),(len g)))) >= Sum (g | (min ((len f),(len g)))) by A4, INTEGRA5:3; :: thesis: verum

end;

end;