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

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then seq . (n + 1) = z * ((seq . 0) * ((z GeoSeq) . n)) by A2
.= (seq . 0) * (z * ((z GeoSeq) . n))
.= (seq . 0) * ((z GeoSeq) . (n + 1)) by Def1 ;
hence S₁[n + 1] ; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z))
seq . 0 = (seq . 0) * 1r by COMPLEX1:def 4
.= (seq . 0) * ((z GeoSeq) . 0) by Def1 ;
then A4: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A3);
then Partial_Sums seq = Partial_Sums ((seq . 0) (#) (z GeoSeq)) by VALUED_1:7
.= (seq . 0) (#) (Partial_Sums (z GeoSeq)) by Th29 ;
hence (Partial_Sums seq) . n = (seq . 0) * ((Partial_Sums (z GeoSeq)) . n) by VALUED_1:6
.= (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) by A1, Th36 ;
:: thesis: verum