let s1, s2 be Real_Sequence; ( 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
; ( 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;
then B2:
Partial_Sums s2 is bounded_above
by SEQ_2:def 3;
hence A7:
s2 is summable
by A3, SERIES_1:17; 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;
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;
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; verum