let F1, F2 be FinSequence of REAL ; :: thesis: ( len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 . i <= F2 . i ) implies Sum F1 <= Sum F2 )
assume that
A1: len F1 = len F2 and
A2: for i being Element of NAT st i in dom F1 holds
F1 . i <= F2 . i ; :: thesis: Sum F1 <= Sum F2
reconsider R1 = F1 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
reconsider R2 = F2 as Element of (len F1) -tuples_on REAL by A1, FINSEQ_2:92;
for i being Nat st i in Seg (len F1) holds
R1 . i <= R2 . i

proof

let i be Nat; :: thesis: ( i in Seg (len F1) implies R1 . i <= R2 . i )
assume i in Seg (len F1) ; :: thesis: R1 . i <= R2 . i
then i in dom F1 by FINSEQ_1:def 3;
hence R1 . i <= R2 . i by A2; :: thesis: verum

end;

hence Sum F1 <= Sum F2 by RVSUM_1:82; :: thesis: verum