let r be real number ; :: thesis: for n being Element of NAT st 0 < r & r < 1 holds
Sum ((r GeoSeq ) ^\ n) = (r |^ n) / (1 - r)
let n be Element of NAT ; :: thesis: ( 0 < r & r < 1 implies Sum ((r GeoSeq ) ^\ n) = (r |^ n) / (1 - r) )
assume A1: ( 0 < r & r < 1 ) ; :: thesis: Sum ((r GeoSeq ) ^\ n) = (r |^ n) / (1 - r)
A2: dom ((r |^ n) (#) (r GeoSeq )) = NAT by FUNCT_2:def 1;

now

let i be Element of NAT ; :: thesis: ((r GeoSeq ) ^\ n) . i = ((r |^ n) (#) (r GeoSeq )) . i
thus ((r GeoSeq ) ^\ n) . i = (r GeoSeq ) . (i + n) by NAT_1:def 3
.= r |^ (i + n) by PREPOWER:def 1
.= (r |^ n) * (r |^ i) by NEWTON:13
.= (r |^ n) * ((r GeoSeq ) . i) by PREPOWER:def 1
.= ((r |^ n) (#) (r GeoSeq )) . i by A2, VALUED_1:def 5 ; :: thesis: verum

end;

then A3: (r GeoSeq ) ^\ n = (r |^ n) (#) (r GeoSeq ) by FUNCT_2:113;
abs r = r by A1, ABSVALUE:def 1;
then ( Sum (r GeoSeq ) = 1 / (1 - r) & r GeoSeq is summable ) by A1, SERIES_1:28;
hence Sum ((r GeoSeq ) ^\ n) = (r |^ n) * (1 / (1 - r)) by A3, SERIES_1:13
.= ((r |^ n) * 1) / (1 - r) by XCMPLX_1:75
.= (r |^ n) / (1 - r) ;
:: thesis: verum