let z be Complex; :: thesis: ( 1r <> z implies for n being Nat holds (Partial_Sums (z GeoSeq)) . n = (1r - (z |^ (n + 1))) / (1r - z) )

now :: thesis: for z being Complex st 1r <> z holds
for n being Nat holds S₁[n]

let z be Complex; :: thesis: ( 1r <> z implies for n being Nat holds S₁[n] )
defpred S₁[ Nat] means (Partial_Sums (z GeoSeq)) . $1 = (1r - (z |^ ($1 + 1))) / (1r - z);
assume 1r <> z ; :: thesis: for n being Nat holds S₁[n]
then A1: 1r - z <> 0c ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
hence (Partial_Sums (z GeoSeq)) . (n + 1) = ((1r - (z |^ (n + 1))) / (1r - z)) + ((z |^ (n + 1)) * 1r) by COMPLEX1:def 4, SERIES_1:def 1
.= ((1r - (z |^ (n + 1))) / (1r - z)) + ((z |^ (n + 1)) * ((1r - z) / (1r - z))) by A1, COMPLEX1:def 4, XCMPLX_1:60
.= ((1r - (z |^ (n + 1))) / (1r - z)) + (((z |^ (n + 1)) * (1r - z)) / (1r - z)) by XCMPLX_1:74
.= ((1r - (z |^ (n + 1))) + ((z |^ (n + 1)) - ((z |^ (n + 1)) * z))) / (1r - z) by COMPLEX1:def 4, XCMPLX_1:62
.= (1r - ((z |^ (n + 1)) * z)) / (1r - z)
.= (1r - (z |^ ((n + 1) + 1))) / (1r - z) by NEWTON:6 ;
:: thesis: verum

end;

(Partial_Sums (z GeoSeq)) . 0 = (z GeoSeq) . 0 by SERIES_1:def 1
.= 1r by Def1
.= (1r - (1 * z)) / (1r - z) by A1, COMPLEX1:def 4, XCMPLX_1:60
.= (1r - (z |^ (0 + 1))) / (1r - z) ;
then A3: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2); :: thesis: verum

end;

hence ( 1r <> z implies for n being Nat holds (Partial_Sums (z GeoSeq)) . n = (1r - (z |^ (n + 1))) / (1r - z) ) ; :: thesis: verum