let n, b be Nat; :: thesis: ( b > 1 implies value ((n --> (b -' 1)),b) = (b |^ n) - 1 )
assume A1: b > 1 ; :: thesis: value ((n --> (b -' 1)),b) = (b |^ n) - 1
then A2: b - 1 > 1 - 1 by XREAL_1:14;
set d = n --> (b -' 1);
set g = (b -' 1) (#) (b GeoSeq);
set d9 = ((b -' 1) (#) (b GeoSeq)) | n;
A3: ( dom ((b -' 1) (#) (b GeoSeq)) = NAT & n in NAT ) by FUNCT_2:def 1, ORDINAL1:def 12;
then n c= dom ((b -' 1) (#) (b GeoSeq)) by ORDINAL1:def 2;
then A4: dom (((b -' 1) (#) (b GeoSeq)) | n) = dom (n --> (b -' 1)) by RELAT_1:62;
A5: for i being Nat st i in dom (((b -' 1) (#) (b GeoSeq)) | n) holds
(((b -' 1) (#) (b GeoSeq)) | n) . i = ((n --> (b -' 1)) . i) * (b |^ i)

proof

let i be Nat; :: thesis: ( i in dom (((b -' 1) (#) (b GeoSeq)) | n) implies (((b -' 1) (#) (b GeoSeq)) | n) . i = ((n --> (b -' 1)) . i) * (b |^ i) )
assume A6: i in dom (((b -' 1) (#) (b GeoSeq)) | n) ; :: thesis: (((b -' 1) (#) (b GeoSeq)) | n) . i = ((n --> (b -' 1)) . i) * (b |^ i)
then A7: i in dom ((b -' 1) (#) (b GeoSeq)) by A4, A3;
thus (((b -' 1) (#) (b GeoSeq)) | n) . i = ((b -' 1) (#) (b GeoSeq)) . i by A6, FUNCT_1:47
.= (b -' 1) * ((b GeoSeq) . i) by A7, VALUED_1:def 5
.= ((n --> (b -' 1)) . i) * ((b GeoSeq) . i) by A6, A4, FUNCOP_1:7
.= ((n --> (b -' 1)) . i) * (b |^ i) by PREPOWER:def 1 ; :: thesis: verum

end;

rng (((b -' 1) (#) (b GeoSeq)) | n) c= NAT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng (((b -' 1) (#) (b GeoSeq)) | n) or o in NAT )
assume o in rng (((b -' 1) (#) (b GeoSeq)) | n) ; :: thesis: o in NAT
then consider a being object such that
A8: ( a in dom (((b -' 1) (#) (b GeoSeq)) | n) & o = (((b -' 1) (#) (b GeoSeq)) | n) . a ) by FUNCT_1:def 3;
reconsider a = a as Nat by A8;
o = ((n --> (b -' 1)) . a) * (b |^ a) by A8, A5
.= (b -' 1) * (b |^ a) by A8, A4, FUNCOP_1:7 ;
hence o in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then ((b -' 1) (#) (b GeoSeq)) | n is NAT -valued by RELAT_1:def 19;
then reconsider d9 = ((b -' 1) (#) (b GeoSeq)) | n as XFinSequence of NAT by AFINSQ_1:5, A4;

per cases ( n = 0 or n <> 0 ) ;

suppose A9: n = 0 ; :: thesis: value ((n --> (b -' 1)),b) = (b |^ n) - 1

then n --> (b -' 1) = {} ;
hence value ((n --> (b -' 1)),b) = 1 - 1 by Th1
.= (b |^ n) - 1 by A9, NEWTON:4 ;
:: thesis: verum

end;

suppose n <> 0 ; :: thesis: value ((n --> (b -' 1)),b) = (b |^ n) - 1

then consider m being Nat such that
A10: n = m + 1 by NAT_1:6;
dom (Partial_Sums (b GeoSeq)) = NAT by PARTFUN1:def 2;
then dom ((b -' 1) (#) (Partial_Sums (b GeoSeq))) = NAT by VALUED_1:def 5;
then A11: m in dom ((b -' 1) (#) (Partial_Sums (b GeoSeq))) by ORDINAL1:def 12;
d9 = ((b -' 1) (#) (b GeoSeq)) | (Segm (m + 1)) by A10;
then Sum d9 = (Partial_Sums ((b -' 1) (#) (b GeoSeq))) . m by RVSUM_4:4
.= ((b -' 1) (#) (Partial_Sums (b GeoSeq))) . m by SERIES_1:9
.= (b -' 1) * ((Partial_Sums (b GeoSeq)) . m) by A11, VALUED_1:def 5
.= (b -' 1) * ((1 - (b to_power n)) / (1 - b)) by A10, SERIES_1:22, A1
.= (b - 1) * ((- ((b |^ n) - 1)) / (- (b - 1))) by A2, XREAL_0:def 2
.= (b - 1) * (((b |^ n) - 1) / (b - 1)) by XCMPLX_1:191
.= (b |^ n) - 1 by XCMPLX_1:87, A2 ;
hence value ((n --> (b -' 1)),b) = (b |^ n) - 1 by A4, A5, NUMERAL1:def 1; :: thesis: verum

end;

end;