let r be real number ; :: thesis: for X being set st 0 < r & r < 1 holds
Sum (X -powers r) <= Sum (r GeoSeq )
let X be set ; :: thesis: ( 0 < r & r < 1 implies Sum (X -powers r) <= Sum (r GeoSeq ) )
assume A1: ( 0 < r & r < 1 ) ; :: thesis: Sum (X -powers r) <= Sum (r GeoSeq )
then abs r = r by ABSVALUE:def 1;
then A2: r GeoSeq is summable by A1, SERIES_1:28;

now

let n be Element of NAT ; :: thesis: ( 0 <= (X -powers r) . n & (X -powers r) . n <= (r GeoSeq ) . n )
A3: ( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;
hence 0 <= (X -powers r) . n by A1, PREPOWER:13; :: thesis: (X -powers r) . n <= (r GeoSeq ) . n
(r GeoSeq ) . n = r |^ n by PREPOWER:def 1;
hence (X -powers r) . n <= (r GeoSeq ) . n by A1, A3, PREPOWER:13; :: thesis: verum

end;

hence Sum (X -powers r) <= Sum (r GeoSeq ) by A2, SERIES_1:24; :: thesis: verum