let z be Element of COMPLEX ; :: thesis: ( |.z.| < 1 implies ( z GeoSeq is summable & Sum (z GeoSeq ) = 1r / (1r - z) ) )
assume A1: |.z.| < 1 ; :: thesis: ( z GeoSeq is summable & Sum (z GeoSeq ) = 1r / (1r - z) )
deffunc H₁( Element of NAT ) -> Element of COMPLEX = z #N ($1 + 1);
consider seq1 being Complex_Sequence such that
A2: for n being Element of NAT holds seq1 . n = H₁(n) from COMSEQ_1:sch 1();
A3: ( seq1 is convergent & lim seq1 = 0c ) by A1, A2, Th44;
set seq2 = NAT --> 1r ;
A4: for n being Element of NAT holds (NAT --> 1r ) . n = 1r by FUNCOP_1:13;
then A5: NAT --> 1r is convergent by COMSEQ_2:9;
then A6: (NAT --> 1r ) - seq1 is convergent by A3, COMSEQ_2:25;
A7: lim ((NAT --> 1r ) - seq1) = (lim (NAT --> 1r )) - (lim seq1) by A3, A5, COMSEQ_2:26
.= 1r by A3, A4, COMSEQ_2:10 ;
A8: (1r / (1r - z)) (#) ((NAT --> 1r ) - seq1) is convergent by A6;
A9: lim ((1r / (1r - z)) (#) ((NAT --> 1r ) - seq1)) = (1r / (1r - z)) * 1r by A6, A7, COMSEQ_2:18
.= 1r / (1r - z) by COMPLEX1:def 7 ;

A10: 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 A1, Th36, COMPLEX1:134
.= (1r - (seq1 . n)) / (1r - z) by A2
.= (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;

hence Partial_Sums (z GeoSeq ) is convergent by A8, FUNCT_2:113; :: according to COMSEQ_3:def 10 :: thesis: Sum (z GeoSeq ) = 1r / (1r - z)
thus Sum (z GeoSeq ) = 1r / (1r - z) by A9, A10, FUNCT_2:113; :: thesis: verum