let z be Element of COMPLEX ; :: thesis: ( 1r <> z implies for n being Element of NAT holds (Partial_Sums (z GeoSeq )) . n = (1r - (z #N (n + 1))) / (1r - z) )

now

let z be Element of COMPLEX ; :: thesis: ( 1r <> z implies for n being Element of NAT holds S₁[n] )
assume 1r <> z ; :: thesis: for n being Element of NAT holds S₁[n]
then A1: 1r - z <> 0c ;
defpred S₁[ Element of NAT ] means (Partial_Sums (z GeoSeq )) . $1 = (1r - (z #N ($1 + 1))) / (1r - z);
A2: S₁[ 0 ]

proof

thus (Partial_Sums (z GeoSeq )) . 0 = (z GeoSeq ) . 0 by Def7
.= 1r by Def1
.= (1r - (1 * z)) / (1r - z) by A1, COMPLEX1:def 7, XCMPLX_1:60
.= (1r - (z #N (0 + 1))) / (1r - z) by NEWTON:10 ; :: thesis: verum

end;

A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of 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 (n + 1))) / (1r - z)) + ((z #N (n + 1)) * 1r ) by Def7, COMPLEX1:def 7
.= ((1r - (z #N (n + 1))) / (1r - z)) + ((z #N (n + 1)) * ((1r - z) / (1r - z))) by A1, COMPLEX1:def 7, XCMPLX_1:60
.= ((1r - (z #N (n + 1))) / (1r - z)) + (((z #N (n + 1)) * (1r - z)) / (1r - z)) by XCMPLX_1:75
.= ((1r - (z #N (n + 1))) + ((z #N (n + 1)) - ((z #N (n + 1)) * z))) / (1r - z) by COMPLEX1:def 7, XCMPLX_1:63
.= (1r - ((z #N (n + 1)) * z)) / (1r - z)
.= (1r - (z #N ((n + 1) + 1))) / (1r - z) by NEWTON:11 ;
:: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3); :: thesis: verum

end;

hence ( 1r <> z implies for n being Element of NAT holds (Partial_Sums (z GeoSeq )) . n = (1r - (z #N (n + 1))) / (1r - z) ) ; :: thesis: verum