let seq be Complex_Sequence; :: thesis: for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds
( seq is summable & Sum seq = (seq . 0 ) / (1r - z) )
let z be Element of COMPLEX ; :: thesis: ( |.z.| < 1 & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) implies ( seq is summable & Sum seq = (seq . 0 ) / (1r - z) ) )
assume that
A1: |.z.| < 1 and
A2: for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ; :: thesis: ( seq is summable & Sum seq = (seq . 0 ) / (1r - z) )

now

let n be Element of NAT ; :: thesis: (Partial_Sums seq) . n = ((seq . 0 ) (#) (Partial_Sums (z GeoSeq ))) . n
thus (Partial_Sums seq) . n = (seq . 0 ) * ((1r - (z #N (n + 1))) / (1r - z)) by A1, A2, Th37, COMPLEX1:134
.= (seq . 0 ) * ((Partial_Sums (z GeoSeq )) . n) by A1, Th36, COMPLEX1:134
.= ((seq . 0 ) (#) (Partial_Sums (z GeoSeq ))) . n by VALUED_1:6 ; :: thesis: verum

end;

then A3: Partial_Sums seq = (seq . 0 ) (#) (Partial_Sums (z GeoSeq )) by FUNCT_2:113;
A4: z GeoSeq is summable by A1, Th65;
hence seq is summable by A3, Def10; :: thesis: Sum seq = (seq . 0 ) / (1r - z)
Sum seq = (seq . 0 ) * (Sum (z GeoSeq )) by A3, A4, COMSEQ_2:18
.= (seq . 0 ) * (1r / (1r - z)) by A1, Th65
.= ((seq . 0 ) * 1r ) / (1r - z) by XCMPLX_1:75
.= (seq . 0 ) / (1r - z) by COMPLEX1:def 7 ;
hence Sum seq = (seq . 0 ) / (1r - z) ; :: thesis: verum