:: LOPBAN_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X be non empty NORMSTR ;
let seq be sequence of X;
func Partial_Sums seq -> sequence of X means :Def1: :: LOPBAN_3:def 1
( it . 0 = seq . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (seq . (n + 1)) ) );
existence
ex b1 being sequence of X st
( b1 . 0 = seq . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (seq . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being sequence of X st b1 . 0 = seq . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (seq . (n + 1)) ) & b2 . 0 = seq . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (seq . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Partial_Sums LOPBAN_3:def 1 :
for X being non empty NORMSTR
for seq, b3 being sequence of X holds
( b3 = Partial_Sums seq iff ( b3 . 0 = seq . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . n) + (seq . (n + 1)) ) ) );

theorem Th1: :: LOPBAN_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty add-associative right_zeroed right_complementable NORMSTR
for seq being sequence of X st ( for n being Nat holds seq . n = 0. X ) holds
for m being Nat holds (Partial_Sums seq) . m = 0. X
proof end;

definition
let X be RealNormSpace;
let seq be sequence of X;
attr seq is summable means :Def2: :: LOPBAN_3:def 2
Partial_Sums seq is convergent;
end;

:: deftheorem Def2 defines summable LOPBAN_3:def 2 :
for X being RealNormSpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );

registration
let X be RealNormSpace;
cluster summable M5( NAT ,the carrier of X);
existence
ex b1 being sequence of X st b1 is summable
proof end;
end;

definition
let X be RealNormSpace;
let seq be sequence of X;
func Sum seq -> Element of X equals :: LOPBAN_3:def 3
lim (Partial_Sums seq);
correctness
coherence
lim (Partial_Sums seq) is Element of X
;
;
end;

:: deftheorem defines Sum LOPBAN_3:def 3 :
for X being RealNormSpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

definition
let X be RealNormSpace;
let seq be sequence of X;
attr seq is norm_summable means :Def4: :: LOPBAN_3:def 4
||.seq.|| is summable;
end;

:: deftheorem Def4 defines norm_summable LOPBAN_3:def 4 :
for X being RealNormSpace
for seq being sequence of X holds
( seq is norm_summable iff ||.seq.|| is summable );

theorem Th2: :: LOPBAN_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for m being Nat holds 0 <= ||.seq.|| . m
proof end;

theorem Th3: :: LOPBAN_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||
proof end;

theorem Th4: :: LOPBAN_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X st seq is convergent holds
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s
proof end;

theorem Th5: :: LOPBAN_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X holds
( seq is CCauchy iff for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p )
proof end;

theorem Th6: :: LOPBAN_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X st ( for n being Nat holds seq . n = 0. X ) holds
for m being Nat holds (Partial_Sums ||.seq.||) . m = 0
proof end;

definition
let X be RealNormSpace;
let seq be sequence of X;
:: original: constant
redefine attr seq is constant means :Def5: :: LOPBAN_3:def 5
ex r being Element of X st
for n being Nat holds seq . n = r;
compatibility
( seq is constant iff ex r being Element of X st
for n being Nat holds seq . n = r )
proof end;
end;

:: deftheorem Def5 defines constant LOPBAN_3:def 5 :
for X being RealNormSpace
for seq being sequence of X holds
( seq is constant iff ex r being Element of X st
for n being Nat holds seq . n = r );

definition
let X be RealNormSpace;
let seq be sequence of X;
let k be Nat;
func seq ^\ k -> sequence of X means :Def6: :: LOPBAN_3:def 6
for n being Nat holds it . n = seq . (n + k);
existence
ex b1 being sequence of X st
for n being Nat holds b1 . n = seq . (n + k)
proof end;
uniqueness
for b1, b2 being sequence of X st ( for n being Nat holds b1 . n = seq . (n + k) ) & ( for n being Nat holds b2 . n = seq . (n + k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines ^\ LOPBAN_3:def 6 :
for X being RealNormSpace
for seq being sequence of X
for k being Nat
for b4 being sequence of X holds
( b4 = seq ^\ k iff for n being Nat holds b4 . n = seq . (n + k) );

definition
let X be non empty 1-sorted ;
let Nseq be increasing Seq_of_Nat;
let seq be sequence of X;
:: original: *
redefine func seq * Nseq -> Function of NAT ,the carrier of X;
coherence
Nseq * seq is Function of NAT ,the carrier of X
proof end;
end;

definition
let X be non empty 1-sorted ;
let Nseq be increasing Seq_of_Nat;
let seq be sequence of X;
:: original: *
redefine func seq * Nseq -> sequence of X;
coherence
Nseq * seq is sequence of X
proof end;
end;

theorem Th7: :: LOPBAN_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty 1-sorted
for seq being sequence of X
for Nseq being increasing Seq_of_Nat
for n being Nat holds (seq * Nseq) . n = seq . (Nseq . n)
proof end;

theorem Th8: :: LOPBAN_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X holds seq ^\ 0 = seq
proof end;

theorem :: LOPBAN_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for k, m being Nat holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
proof end;

theorem Th10: :: LOPBAN_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for k, m being Nat holds (seq ^\ k) ^\ m = seq ^\ (k + m)
proof end;

theorem Th11: :: LOPBAN_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent
proof end;

theorem Th12: :: LOPBAN_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof end;

Lm1: for n, m being Nat st n < m holds
ex k being Nat st m = (n + 1) + k
proof end;

Lm2: for seq being Real_Sequence holds
( ( ( for n being Nat holds seq . n < seq . (n + 1) ) implies for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) & ( ( for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Nat st n < m holds
seq . n < seq . m ) & ( ( for n, m being Nat st n < m holds
seq . n < seq . m ) implies for n being Nat holds seq . n < seq . (n + 1) ) )
proof end;

Lm3: for f being Real_Sequence holds
( f is increasing iff for n being Nat holds f . n < f . (n + 1) )
proof end;

theorem Th13: :: LOPBAN_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for k being Nat holds seq ^\ k is subsequence of seq
proof end;

theorem Th14: :: LOPBAN_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq, seq1 being sequence of X
for k being Nat st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq )
proof end;

theorem Th15: :: LOPBAN_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent
proof end;

theorem Th16: :: LOPBAN_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
lim seq1 = lim seq
proof end;

theorem Th17: :: LOPBAN_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X st seq is constant holds
seq is convergent
proof end;

theorem Th18: :: LOPBAN_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X st ( for n being Nat holds seq . n = 0. X ) holds
seq is norm_summable
proof end;

registration
let X be RealNormSpace;
cluster norm_summable M5( NAT ,the carrier of X);
existence
ex b1 being sequence of X st b1 is norm_summable
proof end;
end;

theorem Th19: :: LOPBAN_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for s being sequence of X st s is summable holds
( s is convergent & lim s = 0. X )
proof end;

theorem Th20: :: LOPBAN_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)
proof end;

theorem Th21: :: LOPBAN_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
proof end;

registration
let X be RealNormSpace;
let seq be norm_summable sequence of X;
cluster ||.seq.|| -> summable ;
coherence
||.seq.|| is summable
by Def4;
end;

registration
let X be RealNormSpace;
cluster summable -> convergent M5( NAT ,the carrier of X);
coherence
for b1 being sequence of X st b1 is summable holds
b1 is convergent
by Th19;
end;

theorem Th22: :: LOPBAN_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
proof end;

theorem Th23: :: LOPBAN_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
proof end;

registration
let X be RealNormSpace;
let seq1, seq2 be summable sequence of X;
cluster seq1 + seq2 -> convergent summable ;
coherence
seq1 + seq2 is summable
by Th22;
cluster seq1 - seq2 -> convergent summable ;
coherence
seq1 - seq2 is summable
by Th23;
end;

theorem Th24: :: LOPBAN_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
proof end;

theorem Th25: :: LOPBAN_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being summable sequence of X
for z being Real holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
proof end;

registration
let X be RealNormSpace;
let z be Real;
let seq be summable sequence of X;
cluster z * seq -> convergent summable ;
coherence
z * seq is summable
by Th25;
end;

theorem Th26: :: LOPBAN_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for s, s1 being sequence of X st ( for n being Nat holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1
proof end;

theorem Th27: :: LOPBAN_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for s being sequence of X st s is summable holds
for n being Nat holds s ^\ n is summable
proof end;

registration
let X be RealNormSpace;
let seq be summable sequence of X;
let n be Nat;
cluster seq ^\ n -> convergent summable ;
coherence
seq ^\ n is summable
by Th27;
end;

theorem Th28: :: LOPBAN_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X holds
( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )
proof end;

registration
let X be RealNormSpace;
let seq be norm_summable sequence of X;
cluster Partial_Sums ||.seq.|| -> bounded_above ;
coherence
Partial_Sums ||.seq.|| is bounded_above
by Th28;
end;

theorem Th29: :: LOPBAN_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealBanachSpace
for seq being sequence of X holds
( seq is summable iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p )
proof end;

theorem Th30: :: LOPBAN_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for s being sequence of X
for n, m being Nat st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
proof end;

theorem Th31: :: LOPBAN_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealBanachSpace
for seq being sequence of X st seq is norm_summable holds
seq is summable
proof end;

theorem :: LOPBAN_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for rseq1 being Real_Sequence
for seq2 being sequence of X st rseq1 is summable & ex m being Nat st
for n being Nat st m <= n holds
||.(seq2 . n).|| <= rseq1 . n holds
seq2 is norm_summable
proof end;

theorem :: LOPBAN_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq1, seq2 being sequence of X st ( for n being Nat holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable holds
( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| )
proof end;

theorem :: LOPBAN_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X st ( for n being Nat holds ||.seq.|| . n > 0 ) & ex m being Nat st
for n being Nat st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable
proof end;

theorem :: LOPBAN_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
proof end;

theorem :: LOPBAN_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Nat st
for n being Nat st m <= n holds
rseq1 . n >= 1 holds
not ||.seq.|| is summable
proof end;

theorem :: LOPBAN_3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds
not seq is norm_summable
proof end;

theorem :: LOPBAN_3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds
( seq is norm_summable iff rseq1 is summable )
proof end;

theorem :: LOPBAN_3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for p being Real st p > 1 & ( for n being Nat st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
seq is norm_summable
proof end;

theorem :: LOPBAN_3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for p being Real st p <= 1 & ( for n being Nat st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
not seq is norm_summable
proof end;

theorem :: LOPBAN_3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Nat holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
proof end;

theorem :: LOPBAN_3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealNormSpace
for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being Nat st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable
proof end;

registration
let X be RealBanachSpace;
cluster norm_summable -> convergent summable M5( NAT ,the carrier of X);
coherence
for b1 being sequence of X st b1 is norm_summable holds
b1 is summable
by Th31;
end;

theorem Th43: :: LOPBAN_3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Banach_Algebra
for x, y, z being Element of X
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
proof end;

definition
let X be non empty multLoopStr ;
let v be Element of X;
canceled;
attr v is invertible means :Def8: :: LOPBAN_3:def 8
ex w being Element of X st
( v * w = 1. X & w * v = 1. X );
end;

:: deftheorem LOPBAN_3:def 7 :
canceled;

:: deftheorem Def8 defines invertible LOPBAN_3:def 8 :
for X being non empty multLoopStr
for v being Element of X holds
( v is invertible iff ex w being Element of X st
( v * w = 1. X & w * v = 1. X ) );

definition
let X be non empty Normed_AlgebraStr ;
let S be sequence of X;
let a be Element of X;
func a * S -> sequence of X means :: LOPBAN_3:def 9
for n being Nat holds it . n = a * (S . n);
existence
ex b1 being sequence of X st
for n being Nat holds b1 . n = a * (S . n)
proof end;
uniqueness
for b1, b2 being sequence of X st ( for n being Nat holds b1 . n = a * (S . n) ) & ( for n being Nat holds b2 . n = a * (S . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines * LOPBAN_3:def 9 :
for X being non empty Normed_AlgebraStr
for S being sequence of X
for a being Element of X
for b4 being sequence of X holds
( b4 = a * S iff for n being Nat holds b4 . n = a * (S . n) );

definition
let X be non empty Normed_AlgebraStr ;
let S be sequence of X;
let a be Element of X;
func S * a -> sequence of X means :: LOPBAN_3:def 10
for n being Nat holds it . n = (S . n) * a;
existence
ex b1 being sequence of X st
for n being Nat holds b1 . n = (S . n) * a
proof end;
uniqueness
for b1, b2 being sequence of X st ( for n being Nat holds b1 . n = (S . n) * a ) & ( for n being Nat holds b2 . n = (S . n) * a ) holds
b1 = b2
proof end;
end;

:: deftheorem defines * LOPBAN_3:def 10 :
for X being non empty Normed_AlgebraStr
for S being sequence of X
for a being Element of X
for b4 being sequence of X holds
( b4 = S * a iff for n being Nat holds b4 . n = (S . n) * a );

definition
let X be non empty Normed_AlgebraStr ;
let seq1, seq2 be sequence of X;
func seq1 * seq2 -> sequence of X means :: LOPBAN_3:def 11
for n being Nat holds it . n = (seq1 . n) * (seq2 . n);
existence
ex b1 being sequence of X st
for n being Nat holds b1 . n = (seq1 . n) * (seq2 . n)
proof end;
uniqueness
for b1, b2 being sequence of X st ( for n being Nat holds b1 . n = (seq1 . n) * (seq2 . n) ) & ( for n being Nat holds b2 . n = (seq1 . n) * (seq2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines * LOPBAN_3:def 11 :
for X being non empty Normed_AlgebraStr
for seq1, seq2, b4 being sequence of X holds
( b4 = seq1 * seq2 iff for n being Nat holds b4 . n = (seq1 . n) * (seq2 . n) );

definition
let X be Banach_Algebra;
let x be Element of X;
assume A1: x is invertible ;
func x " -> Element of X means :Def12: :: LOPBAN_3:def 12
( x * it = 1. X & it * x = 1. X );
existence
ex b1 being Element of X st
( x * b1 = 1. X & b1 * x = 1. X )
by A1, Def8;
uniqueness
for b1, b2 being Element of X st x * b1 = 1. X & b1 * x = 1. X & x * b2 = 1. X & b2 * x = 1. X holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines " LOPBAN_3:def 12 :
for X being Banach_Algebra
for x being Element of X st x is invertible holds
for b3 being Element of X holds
( b3 = x " iff ( x * b3 = 1. X & b3 * x = 1. X ) );

definition
let X be Banach_Algebra;
let z be Element of X;
func z GeoSeq -> sequence of X means :Def13: :: LOPBAN_3:def 13
( it . 0 = 1. X & ( for n being Nat holds it . (n + 1) = (it . n) * z ) );
existence
ex b1 being sequence of X st
( b1 . 0 = 1. X & ( for n being Nat holds b1 . (n + 1) = (b1 . n) * z ) )
proof end;
uniqueness
for b1, b2 being sequence of X st b1 . 0 = 1. X & ( for n being Nat holds b1 . (n + 1) = (b1 . n) * z ) & b2 . 0 = 1. X & ( for n being Nat holds b2 . (n + 1) = (b2 . n) * z ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines GeoSeq LOPBAN_3:def 13 :
for X being Banach_Algebra
for z being Element of X
for b3 being sequence of X holds
( b3 = z GeoSeq iff ( b3 . 0 = 1. X & ( for n being Nat holds b3 . (n + 1) = (b3 . n) * z ) ) );

definition
let X be Banach_Algebra;
let z be Element of X;
let n be Nat;
func z #N n -> Element of X equals :: LOPBAN_3:def 14
(z GeoSeq ) . n;
correctness
coherence
(z GeoSeq ) . n is Element of X
;
;
end;

:: deftheorem defines #N LOPBAN_3:def 14 :
for X being Banach_Algebra
for z being Element of X
for n being Nat holds z #N n = (z GeoSeq ) . n;

theorem :: LOPBAN_3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Banach_Algebra
for z being Element of X holds z #N 0 = 1. X by Def13;

theorem Th45: :: LOPBAN_3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Banach_Algebra
for z being Element of X st ||.z.|| < 1 holds
( z GeoSeq is summable & z GeoSeq is norm_summable )
proof end;

theorem :: LOPBAN_3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Banach_Algebra
for x being Point of X st ||.((1. X) - x).|| < 1 holds
( ((1. X) - x) GeoSeq is summable & ((1. X) - x) GeoSeq is norm_summable ) by Th45;

Lm4: for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
proof end;

Lm5: for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
proof end;

Lm6: for X being RealNormSpace
for x, y being Point of X
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Nat holds ||.(x - y).|| <= seq . n ) holds
x = y
proof end;

theorem :: LOPBAN_3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Banach_Algebra
for x being Point of X st ||.((1. X) - x).|| < 1 holds
( x is invertible & x " = Sum (((1. X) - x) GeoSeq ) )
proof end;