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

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

hence
Sum F1 <= Sum F2
by RVSUM_1:82; :: thesis: verum
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;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