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 A1: ( |.z.| < 1 & ( 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, 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 A2: Partial_Sums seq = (seq . 0 ) (#) (Partial_Sums (z GeoSeq )) by FUNCT_2:113;
( z GeoSeq is summable & Sum (z GeoSeq ) = 1r / (1r - z) ) by A1, Th65;
then A3: ( Partial_Sums (z GeoSeq ) is convergent & Sum (z GeoSeq ) = lim (Partial_Sums (z GeoSeq )) ) ;
then ( Partial_Sums seq is convergent & lim (Partial_Sums seq) = (seq . 0 ) * (lim (Partial_Sums (z GeoSeq ))) ) by A2, COMSEQ_2:18;
hence seq is summable by Def10; :: thesis: Sum seq = (seq . 0 ) / (1r - z)
Sum seq = (seq . 0 ) * (Sum (z GeoSeq )) by A2, A3, 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