:: LOPBAN_3 semantic presentation

definition

let c₁ be non empty NORMSTR ;
let c₂ be sequence of c₁;
func Partial_Sums c₂ -> sequence of a₁ means :Def1: :: LOPBAN_3:def 1
( a₃ . 0 = a₂ . 0 & ( for b₁ being Nat holds a₃ . (b₁ + 1) = (a₃ . b₁) + (a₂ . (b₁ + 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Partial_Sums LOPBAN_3:def 1 :

theorem Th1: :: LOPBAN_3:1

for b₁ being non empty add-associative right_zeroed right_complementable NORMSTR
for b₂ being sequence of b₁ st ( for b₃ being Nat holds b₂ . b₃ = 0. b₁ ) holds
for b₃ being Nat holds (Partial_Sums b₂) . b₃ = 0. b₁

proof end;

definition

let c₁ be RealNormSpace;
let c₂ be sequence of c₁;
attr a₂ is summable means :Def2: :: LOPBAN_3:def 2
Partial_Sums a₂ is convergent;

end;

:: deftheorem Def2 defines summable LOPBAN_3:def 2 :

registration

let c₁ be RealNormSpace;
cluster summable M5( NAT ,the carrier of a₁);
existence

proof end;

end;

definition

let c₁ be RealNormSpace;
let c₂ be sequence of c₁;
func Sum c₂ -> Element of a₁ equals :: LOPBAN_3:def 3
lim (Partial_Sums a₂);
correctness ;

end;

:: deftheorem Def3 defines Sum LOPBAN_3:def 3 :

definition

let c₁ be RealNormSpace;
let c₂ be sequence of c₁;
attr a₂ is norm_summable means :Def4: :: LOPBAN_3:def 4
||.a₂.|| is summable;

end;

:: deftheorem Def4 defines norm_summable LOPBAN_3:def 4 :

theorem Th2: :: LOPBAN_3:2

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Nat holds 0 <= ||.b₂.|| . b₃

proof end;

theorem Th3: :: LOPBAN_3:3

for b₁ being RealNormSpace
for b₂, b₃, b₄ being Element of b₁ holds ||.(b₂ - b₃).|| = ||.((b₂ - b₄) + (b₄ - b₃)).||

proof end;

theorem Th4: :: LOPBAN_3:4

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st b₂ is convergent holds
for b₃ being Real st 0 < b₃ holds
ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
||.((b₂ . b₅) - (b₂ . b₄)).|| < b₃

proof end;

theorem Th5: :: LOPBAN_3:5

for b₁ being RealNormSpace
for b₂ being sequence of b₁ holds
( b₂ is CCauchy iff for b₃ being Real st b₃ > 0 holds
ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
||.((b₂ . b₅) - (b₂ . b₄)).|| < b₃ )

proof end;

theorem Th6: :: LOPBAN_3:6

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st ( for b₃ being Nat holds b₂ . b₃ = 0. b₁ ) holds
for b₃ being Nat holds (Partial_Sums ||.b₂.||) . b₃ = 0

proof end;

definition

let c₁ be RealNormSpace;
let c₂ be sequence of c₁;
redefine attr constant as a₂ is constant means :Def5: :: LOPBAN_3:def 5
ex b₁ being Element of a₁ st
for b₂ being Nat holds a₂ . b₂ = b₁;
compatibility

proof end;

end;

:: deftheorem Def5 defines constant LOPBAN_3:def 5 :

definition

let c₁ be RealNormSpace;
let c₂ be sequence of c₁;
let c₃ be Nat;
func c₂ ^\ c₃ -> sequence of a₁ means :Def6: :: LOPBAN_3:def 6
for b₁ being Nat holds a₄ . b₁ = a₂ . (b₁ + a₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines ^\ LOPBAN_3:def 6 :

definition

let c₁ be non empty 1-sorted ;
let c₂ be increasing Seq_of_Nat;
let c₃ be sequence of c₁;
redefine func * as c₃ * c₂ -> Function of NAT ,the carrier of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be increasing Seq_of_Nat;
let c₃ be sequence of c₁;
redefine func * as c₃ * c₂ -> sequence of a₁;
coherence

proof end;

end;

theorem Th7: :: LOPBAN_3:7

for b₁ being non empty 1-sorted
for b₂ being sequence of b₁
for b₃ being increasing Seq_of_Nat
for b₄ being Nat holds (b₂ * b₃) . b₄ = b₂ . (b₃ . b₄)

proof end;

theorem Th8: :: LOPBAN_3:8

for b₁ being RealNormSpace
for b₂ being sequence of b₁ holds b₂ ^\ 0 = b₂

proof end;

theorem Th9: :: LOPBAN_3:9

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds (b₂ ^\ b₃) ^\ b₄ = (b₂ ^\ b₄) ^\ b₃

proof end;

theorem Th10: :: LOPBAN_3:10

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds (b₂ ^\ b₃) ^\ b₄ = b₂ ^\ (b₃ + b₄)

proof end;

theorem Th11: :: LOPBAN_3:11

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₃ is subsequence of b₂ & b₂ is convergent holds
b₃ is convergent

proof end;

theorem Th12: :: LOPBAN_3:12

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₃ is subsequence of b₂ & b₂ is convergent holds
lim b₃ = lim b₂

proof end;

Lemma17: for b₁, b₂ being Nat st b₁ < b₂ holds
ex b₃ being Nat st b₂ = (b₁ + 1) + b₃

proof end;

Lemma18: for b₁ being Real_Sequence holds
( ( ( for b₂ being Nat holds b₁ . b₂ < b₁ . (b₂ + 1) ) implies for b₂, b₃ being Nat holds b₁ . b₂ < b₁ . ((b₂ + 1) + b₃) ) & ( ( for b₂, b₃ being Nat holds b₁ . b₂ < b₁ . ((b₂ + 1) + b₃) ) implies for b₂, b₃ being Nat st b₂ < b₃ holds
b₁ . b₂ < b₁ . b₃ ) & ( ( for b₂, b₃ being Nat st b₂ < b₃ holds
b₁ . b₂ < b₁ . b₃ ) implies for b₂ being Nat holds b₁ . b₂ < b₁ . (b₂ + 1) ) )

proof end;

Lemma19: for b₁ being Real_Sequence holds
( b₁ is increasing iff for b₂ being Nat holds b₁ . b₂ < b₁ . (b₂ + 1) )

proof end;

theorem Th13: :: LOPBAN_3:13

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Nat holds b₂ ^\ b₃ is subsequence of b₂

proof end;

theorem Th14: :: LOPBAN_3:14

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁
for b₄ being Nat st b₂ is convergent holds
( b₂ ^\ b₄ is convergent & lim (b₂ ^\ b₄) = lim b₂ )

proof end;

theorem Th15: :: LOPBAN_3:15

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & ex b₄ being Nat st b₂ = b₃ ^\ b₄ holds
b₃ is convergent

proof end;

theorem Th16: :: LOPBAN_3:16

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & ex b₄ being Nat st b₂ = b₃ ^\ b₄ holds
lim b₃ = lim b₂

proof end;

theorem Th17: :: LOPBAN_3:17

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st b₂ is constant holds
b₂ is convergent

proof end;

theorem Th18: :: LOPBAN_3:18

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st ( for b₃ being Nat holds b₂ . b₃ = 0. b₁ ) holds
b₂ is norm_summable

proof end;

registration

let c₁ be RealNormSpace;
cluster norm_summable M5( NAT ,the carrier of a₁);
existence

proof end;

end;

theorem Th19: :: LOPBAN_3:19

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st b₂ is summable holds
( b₂ is convergent & lim b₂ = 0. b₁ )

proof end;

theorem Th20: :: LOPBAN_3:20

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ holds (Partial_Sums b₂) + (Partial_Sums b₃) = Partial_Sums (b₂ + b₃)

proof end;

theorem Th21: :: LOPBAN_3:21

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ holds (Partial_Sums b₂) - (Partial_Sums b₃) = Partial_Sums (b₂ - b₃)

proof end;

registration

let c₁ be RealNormSpace;
let c₂ be norm_summable sequence of c₁;
cluster ||.a₂.|| -> summable ;
coherence by Def4;

end;

registration

let c₁ be RealNormSpace;
cluster summable -> convergent M5( NAT ,the carrier of a₁);
coherence by Th19;

end;

theorem Th22: :: LOPBAN_3:22

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is summable & b₃ is summable holds
( b₂ + b₃ is summable & Sum (b₂ + b₃) = (Sum b₂) + (Sum b₃) )

proof end;

theorem Th23: :: LOPBAN_3:23

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is summable & b₃ is summable holds
( b₂ - b₃ is summable & Sum (b₂ - b₃) = (Sum b₂) - (Sum b₃) )

proof end;

registration

let c₁ be RealNormSpace;
let c₂, c₃ be summable sequence of c₁;
cluster a₂ + a₃ -> convergent summable ;
coherence by Th22;
cluster a₂ - a₃ -> convergent summable ;
coherence by Th23;

end;

theorem Th24: :: LOPBAN_3:24

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Real holds Partial_Sums (b₃ * b₂) = b₃ * (Partial_Sums b₂)

proof end;

theorem Th25: :: LOPBAN_3:25

for b₁ being RealNormSpace
for b₂ being summable sequence of b₁
for b₃ being Real holds
( b₃ * b₂ is summable & Sum (b₃ * b₂) = b₃ * (Sum b₂) )

proof end;

registration

let c₁ be RealNormSpace;
let c₂ be Real;
let c₃ be summable sequence of c₁;
cluster a₂ * a₃ -> convergent summable ;
coherence by Th25;

end;

theorem Th26: :: LOPBAN_3:26

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st ( for b₄ being Nat holds b₃ . b₄ = b₂ . 0 ) holds
Partial_Sums (b₂ ^\ 1) = ((Partial_Sums b₂) ^\ 1) - b₃

proof end;

theorem Th27: :: LOPBAN_3:27

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st b₂ is summable holds
for b₃ being Nat holds b₂ ^\ b₃ is summable

proof end;

registration

let c₁ be RealNormSpace;
let c₂ be summable sequence of c₁;
let c₃ be Nat;
cluster a₂ ^\ a₃ -> convergent summable ;
coherence by Th27;

end;

theorem Th28: :: LOPBAN_3:28

for b₁ being RealNormSpace
for b₂ being sequence of b₁ holds
( Partial_Sums ||.b₂.|| is bounded_above iff b₂ is norm_summable )

proof end;

registration

let c₁ be RealNormSpace;
let c₂ be norm_summable sequence of c₁;
cluster Partial_Sums ||.a₂.|| -> bounded_above ;
coherence by Th28;

end;

theorem Th29: :: LOPBAN_3:29

for b₁ being RealBanachSpace
for b₂ being sequence of b₁ holds
( b₂ is summable iff for b₃ being Real st 0 < b₃ holds
ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
||.(((Partial_Sums b₂) . b₅) - ((Partial_Sums b₂) . b₄)).|| < b₃ )

proof end;

theorem Th30: :: LOPBAN_3:30

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
||.(((Partial_Sums b₂) . b₄) - ((Partial_Sums b₂) . b₃)).|| <= abs (((Partial_Sums ||.b₂.||) . b₄) - ((Partial_Sums ||.b₂.||) . b₃))

proof end;

theorem Th31: :: LOPBAN_3:31

for b₁ being RealBanachSpace
for b₂ being sequence of b₁ st b₂ is norm_summable holds
b₂ is summable

proof end;

theorem Th32: :: LOPBAN_3:32

for b₁ being RealNormSpace
for b₂ being Real_Sequence
for b₃ being sequence of b₁ st b₂ is summable & ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
||.(b₃ . b₅).|| <= b₂ . b₅ holds
b₃ is norm_summable

proof end;

theorem Th33: :: LOPBAN_3:33

for b₁ being RealNormSpace
for b₂, b₃ being sequence of b₁ st ( for b₄ being Nat holds
( 0 <= ||.b₂.|| . b₄ & ||.b₂.|| . b₄ <= ||.b₃.|| . b₄ ) ) & b₃ is norm_summable holds
( b₂ is norm_summable & Sum ||.b₂.|| <= Sum ||.b₃.|| )

proof end;

theorem Th34: :: LOPBAN_3:34

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st ( for b₃ being Nat holds ||.b₂.|| . b₃ > 0 ) & ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
(||.b₂.|| . (b₄ + 1)) / (||.b₂.|| . b₄) >= 1 holds
not b₂ is norm_summable

proof end;

theorem Th35: :: LOPBAN_3:35

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = b₄ -root (||.b₂.|| . b₄) ) & b₃ is convergent & lim b₃ < 1 holds
b₂ is norm_summable

proof end;

theorem Th36: :: LOPBAN_3:36

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = b₄ -root (||.b₂.|| . b₄) ) & ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
b₃ . b₅ >= 1 holds
not ||.b₂.|| is summable

proof end;

theorem Th37: :: LOPBAN_3:37

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = b₄ -root (||.b₂.|| . b₄) ) & b₃ is convergent & lim b₃ > 1 holds
not b₂ is norm_summable

proof end;

theorem Th38: :: LOPBAN_3:38

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ||.b₂.|| is non-increasing & ( for b₄ being Nat holds b₃ . b₄ = (2 to_power b₄) * (||.b₂.|| . (2 to_power b₄)) ) holds
( b₂ is norm_summable iff b₃ is summable )

proof end;

theorem Th39: :: LOPBAN_3:39

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Real st b₃ > 1 & ( for b₄ being Nat st b₄ >= 1 holds
||.b₂.|| . b₄ = 1 / (b₄ to_power b₃) ) holds
b₂ is norm_summable

proof end;

theorem Th40: :: LOPBAN_3:40

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Real st b₃ <= 1 & ( for b₄ being Nat st b₄ >= 1 holds
||.b₂.|| . b₄ = 1 / (b₄ to_power b₃) ) holds
not b₂ is norm_summable

proof end;

theorem Th41: :: LOPBAN_3:41

for b₁ being RealNormSpace
for b₂ being sequence of b₁
for b₃ being Real_Sequence st ( for b₄ being Nat holds
( b₂ . b₄ <> 0. b₁ & b₃ . b₄ = (||.b₂.|| . (b₄ + 1)) / (||.b₂.|| . b₄) ) ) & b₃ is convergent & lim b₃ < 1 holds
b₂ is norm_summable

proof end;

theorem Th42: :: LOPBAN_3:42

for b₁ being RealNormSpace
for b₂ being sequence of b₁ st ( for b₃ being Nat holds b₂ . b₃ <> 0. b₁ ) & ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
(||.b₂.|| . (b₄ + 1)) / (||.b₂.|| . b₄) >= 1 holds
not b₂ is norm_summable

proof end;

registration

let c₁ be RealBanachSpace;
cluster norm_summable -> convergent summable M5( NAT ,the carrier of a₁);
coherence by Th31;

end;

theorem Th43: :: LOPBAN_3:43

for b₁ being Banach_Algebra
for b₂, b₃, b₄ being Element of b₁
for b₅, b₆ being Real holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. b₁) = b₂ & ex b₇ being Element of b₁ st b₂ + b₇ = 0. b₁ & (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) & 1 * b₂ = b₂ & 0 * b₂ = 0. b₁ & b₅ * (0. b₁) = 0. b₁ & (- 1) * b₂ = - b₂ & b₂ * (1. b₁) = b₂ & (1. b₁) * b₂ = b₂ & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) & b₅ * (b₂ * b₃) = (b₅ * b₂) * b₃ & b₅ * (b₂ + b₃) = (b₅ * b₂) + (b₅ * b₃) & (b₅ + b₆) * b₂ = (b₅ * b₂) + (b₆ * b₂) & (b₅ * b₆) * b₂ = b₅ * (b₆ * b₂) & (b₅ * b₆) * (b₂ * b₃) = (b₅ * b₂) * (b₆ * b₃) & b₅ * (b₂ * b₃) = b₂ * (b₅ * b₃) & (0. b₁) * b₂ = 0. b₁ & b₂ * (0. b₁) = 0. b₁ & b₂ * (b₃ - b₄) = (b₂ * b₃) - (b₂ * b₄) & (b₃ - b₄) * b₂ = (b₃ * b₂) - (b₄ * b₂) & (b₂ + b₃) - b₄ = b₂ + (b₃ - b₄) & (b₂ - b₃) + b₄ = b₂ - (b₃ - b₄) & (b₂ - b₃) - b₄ = b₂ - (b₃ + b₄) & b₂ + b₃ = (b₂ - b₄) + (b₄ + b₃) & b₂ - b₃ = (b₂ - b₄) + (b₄ - b₃) & b₂ = (b₂ - b₃) + b₃ & b₂ = b₃ - (b₃ - b₂) & ( ||.b₂.|| = 0 implies b₂ = 0. b₁ ) & ( b₂ = 0. b₁ implies ||.b₂.|| = 0 ) & ||.(b₅ * b₂).|| = (abs b₅) * ||.b₂.|| & ||.(b₂ + b₃).|| <= ||.b₂.|| + ||.b₃.|| & ||.(b₂ * b₃).|| <= ||.b₂.|| * ||.b₃.|| & ||.(1. b₁).|| = 1 & b₁ is complete )

proof end;

definition

let c₁ be non empty multLoopStr ;
let c₂ be Element of c₁;
canceled;
attr a₂ is invertible means :Def8: :: LOPBAN_3:def 8
ex b₁ being Element of a₁ st
( a₂ * b₁ = 1. a₁ & b₁ * a₂ = 1. a₁ );

end;

:: deftheorem Def7 LOPBAN_3:def 7 :

:: deftheorem Def8 defines invertible LOPBAN_3:def 8 :

definition

let c₁ be non empty Normed_AlgebraStr ;
let c₂ be sequence of c₁;
let c₃ be Element of c₁;
func c₃ * c₂ -> sequence of a₁ means :: LOPBAN_3:def 9
for b₁ being Nat holds a₄ . b₁ = a₃ * (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines * LOPBAN_3:def 9 :

definition

let c₁ be non empty Normed_AlgebraStr ;
let c₂ be sequence of c₁;
let c₃ be Element of c₁;
func c₂ * c₃ -> sequence of a₁ means :: LOPBAN_3:def 10
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) * a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines * LOPBAN_3:def 10 :

definition

let c₁ be non empty Normed_AlgebraStr ;
let c₂, c₃ be sequence of c₁;
func c₂ * c₃ -> sequence of a₁ means :: LOPBAN_3:def 11
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) * (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines * LOPBAN_3:def 11 :

definition

let c₁ be Banach_Algebra;
let c₂ be Element of c₁;
assume E41: c₂ is invertible ;
func c₂ " -> Element of a₁ means :Def12: :: LOPBAN_3:def 12
( a₂ * a₃ = 1. a₁ & a₃ * a₂ = 1. a₁ );
existence by E41, Def8;
uniqueness

proof end;

end;

:: deftheorem Def12 defines " LOPBAN_3:def 12 :

definition

let c₁ be Banach_Algebra;
let c₂ be Element of c₁;
func c₂ GeoSeq -> sequence of a₁ means :Def13: :: LOPBAN_3:def 13
( a₃ . 0 = 1. a₁ & ( for b₁ being Nat holds a₃ . (b₁ + 1) = (a₃ . b₁) * a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines GeoSeq LOPBAN_3:def 13 :

definition

let c₁ be Banach_Algebra;
let c₂ be Element of c₁;
let c₃ be Nat;
func c₂ #N c₃ -> Element of a₁ equals :: LOPBAN_3:def 14
(a₂ GeoSeq ) . a₃;
correctness ;

end;

:: deftheorem Def14 defines #N LOPBAN_3:def 14 :

theorem Th44: :: LOPBAN_3:44

for b₁ being Banach_Algebra
for b₂ being Element of b₁ holds b₂ #N 0 = 1. b₁ by Def13;

theorem Th45: :: LOPBAN_3:45

for b₁ being Banach_Algebra
for b₂ being Element of b₁ st ||.b₂.|| < 1 holds
( b₂ GeoSeq is summable & b₂ GeoSeq is norm_summable )

proof end;

theorem Th46: :: LOPBAN_3:46

for b₁ being Banach_Algebra
for b₂ being Point of b₁ st ||.((1. b₁) - b₂).|| < 1 holds
( ((1. b₁) - b₂) GeoSeq is summable & ((1. b₁) - b₂) GeoSeq is norm_summable ) by Th45;

Lemma44: for b₁ being RealNormSpace
for b₂ being Point of b₁ st ( for b₃ being Real st b₃ > 0 holds
||.b₂.|| < b₃ ) holds
b₂ = 0. b₁

proof end;

Lemma45: for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ st ( for b₄ being Real st b₄ > 0 holds
||.(b₂ - b₃).|| < b₄ ) holds
b₂ = b₃

proof end;

Lemma46: for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁
for b₄ being Real_Sequence st b₄ is convergent & lim b₄ = 0 & ( for b₅ being Nat holds ||.(b₂ - b₃).|| <= b₄ . b₅ ) holds
b₂ = b₃

proof end;

theorem Th47: :: LOPBAN_3:47

for b₁ being Banach_Algebra
for b₂ being Point of b₁ st ||.((1. b₁) - b₂).|| < 1 holds
( b₂ is invertible & b₂ " = Sum (((1. b₁) - b₂) GeoSeq ) )

proof end;