:: by Yasunari Shidama

::

:: Received February 3, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

theorem Th1: :: LOPBAN_3:1

for X being non empty right_complementable add-associative right_zeroed 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

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;

:: deftheorem Def1 defines summable LOPBAN_3:def 1 :

for X being RealNormSpace

for seq being sequence of X holds

( seq is summable iff Partial_Sums seq is convergent );

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;

ex b_{1} being sequence of X st b_{1} is summable

end;
cluster V4() Relation-like NAT -defined the carrier of X -valued Function-like V32( NAT ) V33( NAT , the carrier of X) summable for Element of K32(K33(NAT, the carrier of X));

existence ex b

proof end;

definition

let X be RealNormSpace;

let seq be sequence of X;

correctness

coherence

lim (Partial_Sums seq) is Element of X;

;

end;
let seq be sequence of X;

correctness

coherence

lim (Partial_Sums seq) is Element of X;

;

:: deftheorem defines Sum LOPBAN_3:def 2 :

for X being RealNormSpace

for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

for X being RealNormSpace

for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

:: deftheorem Def3 defines norm_summable LOPBAN_3:def 3 :

for X being RealNormSpace

for seq being sequence of X holds

( seq is norm_summable iff ||.seq.|| is summable );

for X being RealNormSpace

for seq being sequence of X holds

( seq is norm_summable iff ||.seq.|| is summable );

theorem Th3: :: LOPBAN_3:3

for X being RealNormSpace

for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||

for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||

proof end;

theorem Th4: :: LOPBAN_3:4

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

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

for X being RealNormSpace

for seq being sequence of X holds

( seq is Cauchy_sequence_by_Norm 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 )

for seq being sequence of X holds

( seq is Cauchy_sequence_by_Norm 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

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

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;

theorem Th7: :: LOPBAN_3:7

for X being RealNormSpace

for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds

seq1 is convergent

for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds

seq1 is convergent

proof end;

theorem Th8: :: LOPBAN_3:8

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

for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds

lim seq1 = lim seq

proof end;

:: Norm Space versions of SEQ_4_33 - SEQ_4_39

theorem :: LOPBAN_3:9

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 ) by Th7, Th8;

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 ) by Th7, Th8;

theorem Th10: :: LOPBAN_3:10

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

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 Th11: :: LOPBAN_3:11

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

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 Th13: :: LOPBAN_3:13

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

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;

ex b_{1} being sequence of X st b_{1} is norm_summable

end;
cluster V4() Relation-like NAT -defined the carrier of X -valued Function-like V32( NAT ) V33( NAT , the carrier of X) norm_summable for Element of K32(K33(NAT, the carrier of X));

existence ex b

proof end;

:: Norm Space versions of SERIES_1_7 - SERIES_1_16

theorem Th14: :: LOPBAN_3:14

for X being RealNormSpace

for s being sequence of X st s is summable holds

( s is convergent & lim s = 0. X )

for s being sequence of X st s is summable holds

( s is convergent & lim s = 0. X )

proof end;

theorem Th15: :: LOPBAN_3:15

for X being RealNormSpace

for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)

for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)

proof end;

theorem Th16: :: LOPBAN_3:16

for X being RealNormSpace

for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)

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;

coherence

for b_{1} being Real_Sequence st b_{1} = ||.seq.|| holds

b_{1} is summable
by Def3;

end;
let seq be norm_summable sequence of X;

coherence

for b

b

registration

let X be RealNormSpace;

for b_{1} being sequence of X st b_{1} is summable holds

b_{1} is convergent
by Th14;

end;
cluster Function-like V33( NAT , the carrier of X) summable -> convergent for Element of K32(K33(NAT, the carrier of X));

coherence for b

b

theorem Th17: :: LOPBAN_3:17

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) )

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 Th18: :: LOPBAN_3:18

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) )

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;

coherence

seq1 + seq2 is summable by Th17;

coherence

seq1 - seq2 is summable by Th18;

end;
let seq1, seq2 be summable sequence of X;

coherence

seq1 + seq2 is summable by Th17;

coherence

seq1 - seq2 is summable by Th18;

theorem Th19: :: LOPBAN_3:19

for X being RealNormSpace

for seq being sequence of X

for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)

for seq being sequence of X

for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)

proof end;

theorem Th20: :: LOPBAN_3:20

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) )

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;

coherence

z * seq is summable by Th20;

end;
let z be Real;

let seq be summable sequence of X;

coherence

z * seq is summable by Th20;

theorem Th21: :: LOPBAN_3:21

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

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 Th22: :: LOPBAN_3:22

for X being RealNormSpace

for s being sequence of X st s is summable holds

for n being Nat holds s ^\ n is summable

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;

coherence

for b_{1} being sequence of X st b_{1} = seq ^\ n holds

b_{1} is summable
by Th22;

end;
let seq be summable sequence of X;

let n be Nat;

coherence

for b

b

theorem Th23: :: LOPBAN_3:23

for X being RealNormSpace

for seq being sequence of X holds

( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )

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;

coherence

for b_{1} being Real_Sequence st b_{1} = Partial_Sums ||.seq.|| holds

b_{1} is bounded_above
by Th23;

end;
let seq be norm_summable sequence of X;

coherence

for b

b

theorem Th24: :: LOPBAN_3:24

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 ) by Th5, LOPBAN_1:def 15, Th4;

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 ) by Th5, LOPBAN_1:def 15, Th4;

theorem Th25: :: LOPBAN_3:25

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)).|| <= |.(((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)).|

for s being sequence of X

for n, m being Nat st n <= m holds

||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= |.(((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)).|

proof end;

theorem Th26: :: LOPBAN_3:26

for X being RealBanachSpace

for seq being sequence of X st seq is norm_summable holds

seq is summable

for seq being sequence of X st seq is norm_summable holds

seq is summable

proof end;

theorem :: LOPBAN_3:27

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

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:28

theorem :: LOPBAN_3:29

theorem :: LOPBAN_3:30

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

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:31

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

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:32

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

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:33

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 )

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:34

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 by SERIES_1:32;

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 by SERIES_1:32;

theorem :: LOPBAN_3:35

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 by SERIES_1:33;

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 by SERIES_1:33;

theorem :: LOPBAN_3:36

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

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:37

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

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;

for b_{1} being sequence of X st b_{1} is norm_summable holds

b_{1} is summable
by Th26;

end;
cluster Function-like V33( NAT , the carrier of X) norm_summable -> summable for Element of K32(K33(NAT, the carrier of X));

coherence for b

b

theorem Th38: :: LOPBAN_3:38

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).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )

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).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )

proof end;

registration

for b_{1} being Banach_Algebra holds b_{1} is well-unital
end;

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V140() V141() RealNormSpace-like V154() right-distributive right_unital associative Banach_Algebra-like -> well-unital for Normed_AlgebraStr ;

coherence for b

proof end;

definition

let X be non empty well-unital associative multLoopStr ;

let v be Element of X;

( v is invertible iff ex w being Element of X st

( v * w = 1. X & w * v = 1. X ) )

end;
let v be Element of X;

redefine attr v is invertible means :: LOPBAN_3:def 4

ex w being Element of X st

( v * w = 1. X & w * v = 1. X );

compatibility ex w being Element of X st

( v * w = 1. X & w * v = 1. X );

( v is invertible iff ex w being Element of X st

( v * w = 1. X & w * v = 1. X ) )

proof end;

:: deftheorem defines invertible LOPBAN_3:def 4 :

for X being non empty well-unital associative 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 ) );

for X being non empty well-unital associative 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 multMagma ;

let S be sequence of X;

let a be Element of X;

existence

ex b_{1} being sequence of X st

for n being Nat holds b_{1} . n = a * (S . n)

for b_{1}, b_{2} being sequence of X st ( for n being Nat holds b_{1} . n = a * (S . n) ) & ( for n being Nat holds b_{2} . n = a * (S . n) ) holds

b_{1} = b_{2}

ex b_{1} being sequence of X st

for n being Nat holds b_{1} . n = (S . n) * a

for b_{1}, b_{2} being sequence of X st ( for n being Nat holds b_{1} . n = (S . n) * a ) & ( for n being Nat holds b_{2} . n = (S . n) * a ) holds

b_{1} = b_{2}

end;
let S be sequence of X;

let a be Element of X;

existence

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

existence ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines * LOPBAN_3:def 5 :

for X being non empty multMagma

for S being sequence of X

for a being Element of X

for b_{4} being sequence of X holds

( b_{4} = a * S iff for n being Nat holds b_{4} . n = a * (S . n) );

for X being non empty multMagma

for S being sequence of X

for a being Element of X

for b

( b

:: deftheorem defines * LOPBAN_3:def 6 :

for X being non empty multMagma

for S being sequence of X

for a being Element of X

for b_{4} being sequence of X holds

( b_{4} = S * a iff for n being Nat holds b_{4} . n = (S . n) * a );

for X being non empty multMagma

for S being sequence of X

for a being Element of X

for b

( b

definition

let X be non empty multMagma ;

let seq1, seq2 be sequence of X;

ex b_{1} being sequence of X st

for n being Nat holds b_{1} . n = (seq1 . n) * (seq2 . n)

for b_{1}, b_{2} being sequence of X st ( for n being Nat holds b_{1} . n = (seq1 . n) * (seq2 . n) ) & ( for n being Nat holds b_{2} . n = (seq1 . n) * (seq2 . n) ) holds

b_{1} = b_{2}

end;
let seq1, seq2 be sequence of X;

func seq1 * seq2 -> sequence of X means :: LOPBAN_3:def 7

for n being Nat holds it . n = (seq1 . n) * (seq2 . n);

existence for n being Nat holds it . n = (seq1 . n) * (seq2 . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines * LOPBAN_3:def 7 :

for X being non empty multMagma

for seq1, seq2, b_{4} being sequence of X holds

( b_{4} = seq1 * seq2 iff for n being Nat holds b_{4} . n = (seq1 . n) * (seq2 . n) );

for X being non empty multMagma

for seq1, seq2, b

( b

notation
end;

definition

let X be non empty well-unital associative multLoopStr ;

let x be Element of X;

assume A1: x is invertible ;

compatibility

for b_{1} being Element of the carrier of X holds

( b_{1} = x " iff ( x * b_{1} = 1. X & b_{1} * x = 1. X ) )

end;
let x be Element of X;

assume A1: x is invertible ;

compatibility

for b

( b

proof end;

:: deftheorem Def8 defines " LOPBAN_3:def 8 :

for X being non empty well-unital associative multLoopStr

for x being Element of X st x is invertible holds

for b_{3} being Element of the carrier of X holds

( b_{3} = x " iff ( x * b_{3} = 1. X & b_{3} * x = 1. X ) );

for X being non empty well-unital associative multLoopStr

for x being Element of X st x is invertible holds

for b

( b

definition

let X be Banach_Algebra;

let z be Element of X;

ex b_{1} being sequence of X st

( b_{1} . 0 = 1. X & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * z ) )

for b_{1}, b_{2} being sequence of X st b_{1} . 0 = 1. X & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * z ) & b_{2} . 0 = 1. X & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) * z ) holds

b_{1} = b_{2}

end;
let z be Element of X;

func z GeoSeq -> sequence of X means :Def9: :: LOPBAN_3:def 9

( it . 0 = 1. X & ( for n being Nat holds it . (n + 1) = (it . n) * z ) );

existence ( it . 0 = 1. X & ( for n being Nat holds it . (n + 1) = (it . n) * z ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines GeoSeq LOPBAN_3:def 9 :

for X being Banach_Algebra

for z being Element of X

for b_{3} being sequence of X holds

( b_{3} = z GeoSeq iff ( b_{3} . 0 = 1. X & ( for n being Nat holds b_{3} . (n + 1) = (b_{3} . n) * z ) ) );

for X being Banach_Algebra

for z being Element of X

for b

( b

definition

let X be Banach_Algebra;

let z be Element of X;

let n be Nat;

correctness

coherence

(z GeoSeq) . n is Element of X;

;

end;
let z be Element of X;

let n be Nat;

correctness

coherence

(z GeoSeq) . n is Element of X;

;

:: deftheorem defines #N LOPBAN_3:def 10 :

for X being Banach_Algebra

for z being Element of X

for n being Nat holds z #N n = (z GeoSeq) . n;

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:39

theorem Th40: :: LOPBAN_3:40

for X being Banach_Algebra

for z being Element of X st ||.z.|| < 1 holds

( z GeoSeq is summable & z GeoSeq is norm_summable )

for z being Element of X st ||.z.|| < 1 holds

( z GeoSeq is summable & z GeoSeq is norm_summable )

proof end;

theorem :: LOPBAN_3:41

Lm1: 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;

Lm2: 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;

Lm3: 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:42

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) )

for x being Point of X st ||.((1. X) - x).|| < 1 holds

( x is invertible & x " = Sum (((1. X) - x) GeoSeq) )

proof end;