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

A3: now

let n be Element of NAT ; :: thesis: 0 <= (X -powers r) . n
( ( 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: verum

end;

now

take m = 1; :: thesis: for n being Element of NAT st m <= n holds
(X -powers r) . n <= (r GeoSeq ) . n
let n be Element of NAT ; :: thesis: ( m <= n implies (X -powers r) . n <= (r GeoSeq ) . n )
assume m <= n ; :: thesis: (X -powers r) . n <= (r GeoSeq ) . n
A4: (r GeoSeq ) . n = r |^ n by PREPOWER:def 1;
( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;
hence (X -powers r) . n <= (r GeoSeq ) . n by A1, A4, PREPOWER:13; :: thesis: verum

end;

hence X -powers r is summable by A2, A3, SERIES_1:22; :: thesis: verum