theorem LM2: :: LOPBAN13:4
for S being Banach_Algebra
for w being Point of S st ||.w.|| < 1 holds
( (1. S) + w is invertible & (- w) GeoSeq is norm_summable & ((1. S) + w) " = Sum ((- w) GeoSeq) & ||.(((1. S) + w) ").|| <= 1 / (1 - ||.w.||) )