let z be Element of COMPLEX ; :: thesis: ( |.z.| < 1 implies ( z GeoSeq is summable & Sum (z GeoSeq ) = 1r / (1r - z) ) )
set seq2 = NAT --> 1r ;
deffunc H₁( Element of NAT ) -> Element of COMPLEX = z #N ($1 + 1);
consider seq1 being Complex_Sequence such that
A1: for n being Element of NAT holds seq1 . n = H₁(n) from COMSEQ_1:sch 1();
assume A2: |.z.| < 1 ; :: thesis: ( z GeoSeq is summable & Sum (z GeoSeq ) = 1r / (1r - z) )
then A3: lim seq1 = 0c by A1, Th44;

A4: now

let n be Element of NAT ; :: thesis: (Partial_Sums (z GeoSeq )) . n = ((1r / (1r - z)) (#) ((NAT --> 1r ) - seq1)) . n
thus (Partial_Sums (z GeoSeq )) . n = (1r - (z #N (n + 1))) / (1r - z) by A2, Th36, COMPLEX1:134
.= (1r - (seq1 . n)) / (1r - z) by A1
.= (1r * (((NAT --> 1r ) . n) - (seq1 . n))) / (1r - z) by COMPLEX1:def 7, FUNCOP_1:13
.= (1r / (1r - z)) * (((NAT --> 1r ) . n) + (- (seq1 . n))) by XCMPLX_1:75
.= (1r / (1r - z)) * (((NAT --> 1r ) . n) + ((- seq1) . n)) by VALUED_1:8
.= (1r / (1r - z)) * (((NAT --> 1r ) - seq1) . n) by VALUED_1:1
.= ((1r / (1r - z)) (#) ((NAT --> 1r ) - seq1)) . n by VALUED_1:6 ; :: thesis: verum

end;

A5: for n being Element of NAT holds (NAT --> 1r ) . n = 1r by FUNCOP_1:13;
then A6: NAT --> 1r is convergent by COMSEQ_2:9;
A7: seq1 is convergent by A2, A1, Th44;
then A8: (NAT --> 1r ) - seq1 is convergent by A6, COMSEQ_2:25;
hence Partial_Sums (z GeoSeq ) is convergent by A4, FUNCT_2:113; :: according to COMSEQ_3:def 12 :: thesis: Sum (z GeoSeq ) = 1r / (1r - z)
lim ((NAT --> 1r ) - seq1) = (lim (NAT --> 1r )) - (lim seq1) by A7, A6, COMSEQ_2:26
.= 1r by A3, A5, COMSEQ_2:10 ;
then lim ((1r / (1r - z)) (#) ((NAT --> 1r ) - seq1)) = (1r / (1r - z)) * 1r by A8, COMSEQ_2:18
.= 1r / (1r - z) by COMPLEX1:def 7 ;
hence Sum (z GeoSeq ) = 1r / (1r - z) by A4, FUNCT_2:113; :: thesis: verum