for X being Banach_Algebra
for z being Point of X st ||.z.|| < 1 holds
( z GeoSeq is norm_summable & ||.(Sum (z GeoSeq)).|| <= 1 / (1 - ||.z.||) )