let z be Complex; :: thesis: ( |.z.| < 1 implies ( z GeoSeq is summable & Sum (z GeoSeq) = 1r / (1r - z) ) )
set seq2 = NAT --> 1r;
deffunc H₁( Nat) -> Element of COMPLEX = z |^ ($1 + 1);
consider seq1 being Complex_Sequence such that
A1: for n being 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 :: thesis: for n being Element of NAT holds (Partial_Sums (z GeoSeq)) . n = ((1r / (1r - z)) (#) ((NAT --> 1r) - seq1)) . n

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 + 1))) / (1r - z) by A2, Th36, COMPLEX1:48
.= (1r - (seq1 . n)) / (1r - z) by A1
.= (1r * (((NAT --> 1r) . n) - (seq1 . n))) / (1r - z) by COMPLEX1:def 4, FUNCOP_1:7
.= (1r / (1r - z)) * (((NAT --> 1r) . n) + (- (seq1 . n))) by XCMPLX_1:74
.= (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 Nat holds (NAT --> 1r) . n = 1r by ORDINAL1:def 12, FUNCOP_1:7;
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;
hence Partial_Sums (z GeoSeq) is convergent by A4, FUNCT_2:63; :: according to COMSEQ_3:def 8 :: 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 4 ;
hence Sum (z GeoSeq) = 1r / (1r - z) by A4, FUNCT_2:63; :: thesis: verum