let s1, s2 be Real_Sequence; :: thesis: ( s1,s2 are_fiberwise_equipotent & s1 is nonnegative & s1 is summable implies ( s2 is summable & Sum s1 = Sum s2 ) )
assume that
A1: ( s1,s2 are_fiberwise_equipotent & s1 is nonnegative ) and
A2: s1 is summable ; :: thesis: ( s2 is summable & Sum s1 = Sum s2 )
Partial_Sums s1 is bounded_above by A2, A1, SERIES_1:17;
then consider r being Real such that
A5: for n being Nat holds (Partial_Sums s1) . n < r by SEQ_2:def 3;
A3: for n being Nat holds 0 <= s2 . n by A1, TMP6, RINFSUP1:def 3;

B3: now :: thesis: for n being Nat holds (Partial_Sums s2) . n < r

let n be Nat; :: thesis: (Partial_Sums s2) . n < r
consider m being Nat such that
A6: (Partial_Sums s2) . n <= (Partial_Sums s1) . m by A1, TMP6, SH8;
thus (Partial_Sums s2) . n < r by A5, A6, XXREAL_0:2; :: thesis: verum

end;

then B2: Partial_Sums s2 is bounded_above by SEQ_2:def 3;
hence A7: s2 is summable by A3, SERIES_1:17; :: thesis: Sum s1 = Sum s2
A8: ( Partial_Sums s1 is bounded_above & Partial_Sums s2 is bounded_above ) by A2, B3, SEQ_2:def 3, A1, SERIES_1:17;

now :: thesis: for n being Nat holds (Partial_Sums s1) . n <= lim (Partial_Sums s2)

let n be Nat; :: thesis: (Partial_Sums s1) . n <= lim (Partial_Sums s2)
consider m being Nat such that
A11: (Partial_Sums s1) . n <= (Partial_Sums s2) . m by A1, SH8;
(Partial_Sums s2) . m <= lim (Partial_Sums s2) by A3, B2, SERIES_1:16, SEQ_4:37;
hence (Partial_Sums s1) . n <= lim (Partial_Sums s2) by A11, XXREAL_0:2; :: thesis: verum

end;

then lim (Partial_Sums s1) <= lim (Partial_Sums s2) by A2, SERIES_1:def 2, PREPOWER:2;
then Sum s1 <= lim (Partial_Sums s2) by SERIES_1:def 3;
then A12: Sum s1 <= Sum s2 by SERIES_1:def 3;

now :: thesis: for m being Nat holds (Partial_Sums s2) . m <= lim (Partial_Sums s1)

let m be Nat; :: thesis: (Partial_Sums s2) . m <= lim (Partial_Sums s1)
consider n being Nat such that
A13: (Partial_Sums s2) . m <= (Partial_Sums s1) . n by A1, TMP6, SH8;
(Partial_Sums s1) . n <= lim (Partial_Sums s1) by A8, A1, SERIES_1:16, SEQ_4:37;
hence (Partial_Sums s2) . m <= lim (Partial_Sums s1) by A13, XXREAL_0:2; :: thesis: verum

end;

then lim (Partial_Sums s2) <= lim (Partial_Sums s1) by A7, SERIES_1:def 2, PREPOWER:2;
then Sum s2 <= lim (Partial_Sums s1) by SERIES_1:def 3;
then Sum s2 <= Sum s1 by SERIES_1:def 3;
hence Sum s1 = Sum s2 by A12, XXREAL_0:1; :: thesis: verum