let s1, s2 be Real_Sequence; :: thesis: for n being Nat st s1,s2 are_fiberwise_equipotent & s1 is nonnegative holds
ex m being Nat st (Partial_Sums s1) . n <= (Partial_Sums s2) . m
let n be Nat; :: thesis: ( s1,s2 are_fiberwise_equipotent & s1 is nonnegative implies ex m being Nat st (Partial_Sums s1) . n <= (Partial_Sums s2) . m )
assume that
A1: s1,s2 are_fiberwise_equipotent and
A2: s1 is nonnegative ; :: thesis: ex m being Nat st (Partial_Sums s1) . n <= (Partial_Sums s2) . m
B1: s2 is nonnegative by A1, A2, TMP6;
consider m being Nat, F2 being Subset of (Shift ((s2 | (Segm m)),1)) such that
A3: Shift ((s1 | (Segm (n + 1))),1),F2 are_fiberwise_equipotent by A1, SH6;
take m ; :: thesis: (Partial_Sums s1) . n <= (Partial_Sums s2) . m
reconsider FS1 = Shift ((s1 | (Segm (n + 1))),1), FS2 = Shift ((s2 | (Segm m)),1) as FinSequence of REAL by SH2;
reconsider F2 = F2 as Subset of FS2 ;
Seq F2,F2 are_fiberwise_equipotent by SH7;
then A4: Sum FS1 = Sum (Seq F2) by A3, CLASSES1:76, RFINSEQ:9;

now :: thesis: for i being Element of NAT st i in dom FS2 holds
0 <= FS2 . i

let i be Element of NAT ; :: thesis: ( i in dom FS2 implies 0 <= FS2 . i )
assume A6: i in dom FS2 ; :: thesis: 0 <= FS2 . i
then reconsider i1 = i - 1 as Element of NAT by NAT_1:21, FINSEQ_3:25;
i1 + 1 = i ;
then FS2 . i = s2 . i1 by A6, SH3;
hence 0 <= FS2 . i by A1, A2, TMP6, RINFSUP1:def 3; :: thesis: verum

end;

then Sum (Seq F2) <= Sum FS2 by GLIB_003:2;
then A7: (Partial_Sums s1) . n <= Sum FS2 by A4, SH5;
Shift ((s2 | (Segm (m + 1))),1) = (Shift ((s2 | (Segm m)),1)) ^ <*(s2 . m)*> by SH4;
then Sum (Shift ((s2 | (Segm (m + 1))),1)) = (Sum FS2) + (s2 . m) by RVSUM_1:74;
then A8: (Partial_Sums s2) . m = (Sum FS2) + (s2 . m) by SH5;
(Partial_Sums s2) . m >= Sum FS2 by A8, XREAL_1:31, B1;
hence (Partial_Sums s1) . n <= (Partial_Sums s2) . m by A7, XXREAL_0:2; :: thesis: verum