:: SEQ_4 semantic presentation

begin


theorem Th1: :: SEQ_4:1
for X, Y being Subset of REAL st ( for r, p being real number st r in X & p in Y holds
r < p ) holds
ex g being real number st
for r, p being real number st r in X & p in Y holds
( r <= g & g <= p )
proof
let X, Y be Subset of REAL; ::_thesis: ( ( for r, p being real number st r in X & p in Y holds
r < p ) implies ex g being real number st
for r, p being real number st r in X & p in Y holds
( r <= g & g <= p ) )
assume  for r, p being real number st r in X & p in Y holds
r < p ; ::_thesis: ex g being real number st
for r, p being real number st r in X & p in Y holds
( r <= g & g <= p )
then  for r, p being real number st r in X & p in Y holds
r <= p ;
then consider g being real number  such that
A1: for r, p being real number st r in X & p in Y holds
( r <= g & g <= p ) by AXIOMS:1;
reconsider g = g as Real by XREAL_0:def_1;
take  g ; ::_thesis: for r, p being real number st r in X & p in Y holds
( r <= g & g <= p )
thus  for r, p being real number st r in X & p in Y holds
( r <= g & g <= p ) by A1; ::_thesis: verum
end;

theorem Th2: :: SEQ_4:2
for p being real number
for X being Subset of REAL st 0 < p & ex r being real number st r in X & ( for r being real number st r in X holds
r + p in X ) holds
for g being real number ex r being real number st
( r in X & g < r )
proof
let p be real number ; ::_thesis: for X being Subset of REAL st 0 < p & ex r being real number st r in X & ( for r being real number st r in X holds
r + p in X ) holds
for g being real number ex r being real number st
( r in X & g < r )
let X be Subset of REAL; ::_thesis: ( 0 < p & ex r being real number st r in X & ( for r being real number st r in X holds
r + p in X ) implies for g being real number ex r being real number st
( r in X & g < r ) )
assume that
A1: 0 < p and
A2: ex r being real number st r in X and
A3: for r being real number st r in X holds
r + p in X and
A4: ex g being real number st
for r being real number st r in X holds
not g < r ; ::_thesis: contradiction
defpred S1[ Real] means  for r being real number st r in X holds
not $1 < r;
consider Y being Subset of REAL such that
A5: for p1 being Real holds
( p1 in Y iff S1[p1] ) from SUBSET_1:sch_3();
now__::_thesis:_for_r,_p1_being_real_number_st_r_in_X_&_p1_in_Y_holds_
r_<_p1
let r, p1 be real number ; ::_thesis: ( r in X & p1 in Y implies r < p1 )
assume that
A6: r in X and
A7: p1 in Y ; ::_thesis: r < p1
 r + p in X by A3, A6;
then A8: r + p <= p1 by A5, A7;
 r + 0 < r + p by A1, XREAL_1:8;
hence  r < p1 by A8, XXREAL_0:2; ::_thesis: verum
end;
then consider g2 being real number  such that
A9: for r, p1 being real number st r in X & p1 in Y holds
( r <= g2 & g2 <= p1 ) by Th1;
consider g1 being real number  such that
A10: for r being real number st r in X holds
not g1 < r by A4;
 g1 is Real by XREAL_0:def_1;
then A11: g1 in Y by A10, A5;
A12: now__::_thesis:_g2_-_p_in_Y
assume  not g2 - p in Y ; ::_thesis: contradiction
then consider r1 being real number  such that
A13: ( r1 in X & g2 - p < r1 ) by A5;
 ( (g2 - p) + p < r1 + p & r1 + p in X ) by A3, A13, XREAL_1:6;
hence  contradiction by A11, A9; ::_thesis: verum
end;
 - p < - 0 by A1, XREAL_1:24;
then  g2 + (- p) < g2 + 0 by XREAL_1:6;
hence  contradiction by A2, A9, A12; ::_thesis: verum
end;

theorem Th3: :: SEQ_4:3
for r being real number ex n being Element of NAT st r < n
proof
let r be real number ; ::_thesis: ex n being Element of NAT st r < n
 for r being real number st r in NAT holds
r + 1 in NAT by AXIOMS:2;
then consider p being real number  such that
A1: p in NAT and
A2: r < p by Th2;
consider n1 being Element of NAT  such that
A3: n1 = p by A1;
take  n1 ; ::_thesis: r < n1
thus  r < n1 by A2, A3; ::_thesis: verum
end;

theorem :: SEQ_4:4
for X being Subset of REAL holds
( X is real-bounded iff ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) )
proof
let X be Subset of REAL; ::_thesis: ( X is real-bounded iff ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) )
thus  ( X is real-bounded implies ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) ) ::_thesis: ( ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) implies X is real-bounded )
proof
assume A1: X is real-bounded ; ::_thesis: ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) )
then consider s1 being real number  such that
A2: s1 is UpperBound of X by XXREAL_2:def_10;
A3: for r being real number st r in X holds
r <= s1 by A2, XXREAL_2:def_1;
consider s2 being real number  such that
A4: s2 is LowerBound of X by A1, XXREAL_2:def_9;
A5: for r being real number st r in X holds
s2 <= r by A4, XXREAL_2:def_2;
take s = ((abs s1) + (abs s2)) + 1; ::_thesis: ( 0 < s & ( for r being real number st r in X holds
abs r < s ) )
A6: 0 <= abs s1 by COMPLEX1:46;
A7: 0 <= abs s2 by COMPLEX1:46;
hence  0 < s by A6; ::_thesis: for r being real number st r in X holds
abs r < s
let r be real number ; ::_thesis: ( r in X implies abs r < s )
assume A8: r in X ; ::_thesis: abs r < s
 ( s1 <= abs s1 & r <= s1 ) by A3, A8, ABSVALUE:4;
then  r <= abs s1 by XXREAL_0:2;
then  r + 0 <= (abs s1) + (abs s2) by A7, XREAL_1:7;
then A9: r < s by XREAL_1:8;
 ( - (abs s2) <= s2 & s2 <= r ) by A5, A8, ABSVALUE:4;
then  - (abs s2) <= r by XXREAL_0:2;
then  (- (abs s1)) + (- (abs s2)) <= 0 + r by A6, XREAL_1:7;
then A10: ((- (abs s1)) - (abs s2)) + (- 1) < r + 0 by XREAL_1:8;
 ((- (abs s1)) - (abs s2)) - 1 = - (((abs s1) + (abs s2)) + 1) ;
hence  abs r < s by A9, A10, SEQ_2:1; ::_thesis: verum
end;
given s being real number  such that  0 < s and
A11: for r being real number st r in X holds
abs r < s ; ::_thesis: X is real-bounded
thus  X is bounded_below :: according to XXREAL_2:def_11 ::_thesis: X is bounded_above
proof
take  - s ; :: according to XXREAL_2:def_9 ::_thesis: - s is LowerBound of X
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in X or - s <= r )
assume A12: r in X ; ::_thesis: - s <= r
then reconsider r = r as real number ;
 abs r < s by A11, A12;
then A13: - s < - (abs r) by XREAL_1:24;
 - (abs r) <= r by ABSVALUE:4;
hence  - s <= r by A13, XXREAL_0:2; ::_thesis: verum
end;
take  s ; :: according to XXREAL_2:def_10 ::_thesis: s is UpperBound of X
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in X or r <= s )
assume A14: r in X ; ::_thesis: r <= s
then reconsider r = r as real number ;
 r <= abs r by ABSVALUE:4;
hence  r <= s by A11, A14, XXREAL_0:2; ::_thesis: verum
end;

definition
let r be real number ;
:: original: {
redefine func{r} ->  Subset of REAL;
coherence
 {r} is Subset of REAL
proof
 {r} c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {r} or x in REAL )
assume  x in {r} ; ::_thesis: x in REAL
hence  x in REAL by XREAL_0:def_1; ::_thesis: verum
end;
hence  {r} is Subset of REAL ; ::_thesis: verum
end;
end;

theorem Th5: :: SEQ_4:5
for X being real-membered set st not X is empty & X is bounded_above holds
ex g being real number st
( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) )
proof
let X be real-membered set ; ::_thesis: ( not X is empty & X is bounded_above implies ex g being real number st
( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) ) )
assume that
A1: not X is empty and
A2: X is bounded_above ; ::_thesis: ex g being real number st
( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) )
consider p1 being real number  such that
A3: p1 is UpperBound of X by A2, XXREAL_2:def_10;
A4: for r being real number st r in X holds
r <= p1 by A3, XXREAL_2:def_1;
defpred S1[ Real] means  for r being real number st r in X holds
r <= $1;
consider Y being Subset of REAL such that
A5: for p being Real holds
( p in Y iff S1[p] ) from SUBSET_1:sch_3();
 ( X is Subset of REAL & ( for r, p being real number st r in X & p in Y holds
r <= p ) ) by A5, MEMBERED:3;
then consider g1 being real number  such that
A6: for r, p being real number st r in X & p in Y holds
( r <= g1 & g1 <= p ) by AXIOMS:1;
reconsider g1 = g1 as Real by XREAL_0:def_1;
take g = g1; ::_thesis: ( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) )
A7: ex r1 being real number st r1 in X by A1, MEMBERED:9;
A8: now__::_thesis:_for_s1_being_real_number_holds_
(_not_0_<_s1_or_ex_r_being_real_number_st_
(_r_in_X_&_g_-_s1_<_r_)_)
given s1 being real number  such that A9: 0 < s1 and
A10: for r being real number st r in X holds
not g - s1 < r ; ::_thesis: contradiction
 g - s1 in Y by A5, A10;
then  g <= g - s1 by A7, A6;
then  g - (g - s1) <= (g - s1) - (g - s1) by XREAL_1:9;
hence  contradiction by A9; ::_thesis: verum
end;
 p1 is Real by XREAL_0:def_1;
then  p1 in Y by A4, A5;
hence  ( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) ) by A6, A8; ::_thesis: verum
end;

theorem Th6: :: SEQ_4:6
for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
r <= g1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) ) & ( for r being real number st r in X holds
r <= g2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ) holds
g1 = g2
proof
let g1, g2 be real number ; ::_thesis: for X being real-membered set st ( for r being real number st r in X holds
r <= g1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) ) & ( for r being real number st r in X holds
r <= g2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ) holds
g1 = g2
let X be real-membered set ; ::_thesis: ( ( for r being real number st r in X holds
r <= g1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) ) & ( for r being real number st r in X holds
r <= g2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ) implies g1 = g2 )
assume that
A1: for r being real number st r in X holds
r <= g1 and
A2: for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) and
A3: for r being real number st r in X holds
r <= g2 and
A4: for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ; ::_thesis: g1 = g2
A5: now__::_thesis:_not_g2_<_g1
assume  g2 < g1 ; ::_thesis: contradiction
then  ex r1 being real number st
( r1 in X & g1 - (g1 - g2) < r1 ) by A2, XREAL_1:50;
hence  contradiction by A3; ::_thesis: verum
end;
now__::_thesis:_not_g1_<_g2
assume  g1 < g2 ; ::_thesis: contradiction
then  ex r1 being real number st
( r1 in X & g2 - (g2 - g1) < r1 ) by A4, XREAL_1:50;
hence  contradiction by A1; ::_thesis: verum
end;
hence  g1 = g2 by A5, XXREAL_0:1; ::_thesis: verum
end;

theorem Th7: :: SEQ_4:7
for X being real-membered set st not X is empty & X is bounded_below holds
ex g being real number st
( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) )
proof
let X be real-membered set ; ::_thesis: ( not X is empty & X is bounded_below implies ex g being real number st
( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) ) )
assume that
A1: not X is empty and
A2: X is bounded_below ; ::_thesis: ex g being real number st
( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) )
A3: ex r1 being real number st r1 in X by A1, MEMBERED:9;
consider p1 being real number  such that
A4: p1 is LowerBound of X by A2, XXREAL_2:def_9;
A5: for r being real number st r in X holds
p1 <= r by A4, XXREAL_2:def_2;
reconsider X = X as Subset of REAL by MEMBERED:3;
defpred S1[ Real] means  for r being real number st r in X holds
$1 <= r;
consider Y being Subset of REAL such that
A6: for p being Real holds
( p in Y iff S1[p] ) from SUBSET_1:sch_3();
 for p, r being real number st p in Y & r in X holds
p <= r by A6;
then consider g1 being real number  such that
A7: for p, r being real number st p in Y & r in X holds
( p <= g1 & g1 <= r ) by AXIOMS:1;
reconsider g1 = g1 as Real by XREAL_0:def_1;
take g = g1; ::_thesis: ( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) )
A8: now__::_thesis:_for_s1_being_real_number_holds_
(_not_0_<_s1_or_ex_r_being_real_number_st_
(_r_in_X_&_r_<_g_+_s1_)_)
given s1 being real number  such that A9: 0 < s1 and
A10: for r being real number st r in X holds
not r < g + s1 ; ::_thesis: contradiction
 g + s1 in Y by A6, A10;
then  g + s1 <= g by A3, A7;
then  (g + s1) - g <= g - g by XREAL_1:9;
hence  contradiction by A9; ::_thesis: verum
end;
 p1 is Real by XREAL_0:def_1;
then  p1 in Y by A5, A6;
hence  ( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) ) by A7, A8; ::_thesis: verum
end;

theorem Th8: :: SEQ_4:8
for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
g1 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g1 + s ) ) & ( for r being real number st r in X holds
g2 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g2 + s ) ) holds
g1 = g2
proof
let g1, g2 be real number ; ::_thesis: for X being real-membered set st ( for r being real number st r in X holds
g1 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g1 + s ) ) & ( for r being real number st r in X holds
g2 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g2 + s ) ) holds
g1 = g2
let X be real-membered set ; ::_thesis: ( ( for r being real number st r in X holds
g1 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g1 + s ) ) & ( for r being real number st r in X holds
g2 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g2 + s ) ) implies g1 = g2 )
assume that
A1: for r being real number st r in X holds
g1 <= r and
A2: for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g1 + s ) and
A3: for r being real number st r in X holds
g2 <= r and
A4: for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g2 + s ) ; ::_thesis: g1 = g2
A5: now__::_thesis:_not_g2_<_g1
assume  g2 < g1 ; ::_thesis: contradiction
then  ex r1 being real number st
( r1 in X & r1 < g2 + (g1 - g2) ) by A4, XREAL_1:50;
hence  contradiction by A1; ::_thesis: verum
end;
now__::_thesis:_not_g1_<_g2
assume  g1 < g2 ; ::_thesis: contradiction
then  ex r1 being real number st
( r1 in X & r1 < g1 + (g2 - g1) ) by A2, XREAL_1:50;
hence  contradiction by A3; ::_thesis: verum
end;
hence  g1 = g2 by A5, XXREAL_0:1; ::_thesis: verum
end;

definition
let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_above ) ;
func upper_bound X ->  real number  means :Def1: :: SEQ_4:def 1
( ( for r being real number st r in X holds
r <= it ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & it - s < r ) ) );
existence
 ex b1 being real number st
( ( for r being real number st r in X holds
r <= b1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & b1 - s < r ) ) ) by A1, Th5;
uniqueness
 for b1, b2 being real number st ( for r being real number st r in X holds
r <= b1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & b1 - s < r ) ) & ( for r being real number st r in X holds
r <= b2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & b2 - s < r ) ) holds
b1 = b2 by Th6;
end;

:: deftheorem Def1 defines upper_bound SEQ_4:def_1_:_
 for X being real-membered set st not X is empty & X is bounded_above holds
for b2 being real number holds
( b2 = upper_bound X iff ( ( for r being real number st r in X holds
r <= b2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & b2 - s < r ) ) ) );

definition
let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_below ) ;
func lower_bound X ->  real number  means :Def2: :: SEQ_4:def 2
( ( for r being real number st r in X holds
it <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < it + s ) ) );
existence
 ex b1 being real number st
( ( for r being real number st r in X holds
b1 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < b1 + s ) ) ) by A1, Th7;
uniqueness
 for b1, b2 being real number st ( for r being real number st r in X holds
b1 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < b1 + s ) ) & ( for r being real number st r in X holds
b2 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < b2 + s ) ) holds
b1 = b2 by Th8;
end;

:: deftheorem Def2 defines lower_bound SEQ_4:def_2_:_
 for X being real-membered set st not X is empty & X is bounded_below holds
for b2 being real number holds
( b2 = lower_bound X iff ( ( for r being real number st r in X holds
b2 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < b2 + s ) ) ) );

Lm1:  for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X
proof
let r be real number ; ::_thesis: for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X
let X be non empty real-membered set ; ::_thesis: ( ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) implies r = lower_bound X )
assume that
A1: for s being real number st s in X holds
s >= r and
A2: for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ; ::_thesis: r = lower_bound X
A3: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_t_being_real_number_st_
(_t_in_X_&_not_t_>=_r_+_s_)
let s be real number ; ::_thesis: ( 0 < s implies ex t being real number st
( t in X & not t >= r + s ) )
assume A4: 0 < s ; ::_thesis: ex t being real number st
( t in X & not t >= r + s )
assume  for t being real number st t in X holds
t >= r + s ; ::_thesis: contradiction
then  r >= r + s by A2;
hence  contradiction by A4, XREAL_1:29; ::_thesis: verum
end;
 X is bounded_below
proof
take  r ; :: according to XXREAL_2:def_9 ::_thesis: r is LowerBound of X
let s be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not s in X or r <= s )
assume  s in X ; ::_thesis: r <= s
hence  r <= s by A1; ::_thesis: verum
end;
hence  r = lower_bound X by A1, A3, Def2; ::_thesis: verum
end;

Lm2:  for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X
proof
let X be non empty real-membered set ; ::_thesis: for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X
let r be real number ; ::_thesis: ( ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) implies r = upper_bound X )
assume that
A1: for s being real number st s in X holds
s <= r and
A2: for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ; ::_thesis: r = upper_bound X
A3: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_t_being_real_number_st_
(_t_in_X_&_not_r_-_s_>=_t_)
let s be real number ; ::_thesis: ( 0 < s implies ex t being real number st
( t in X & not r - s >= t ) )
assume A4: 0 < s ; ::_thesis: ex t being real number st
( t in X & not r - s >= t )
assume  for t being real number st t in X holds
r - s >= t ; ::_thesis: contradiction
then  r <= r - s by A2;
then  r + s <= r by XREAL_1:19;
hence  contradiction by A4, XREAL_1:29; ::_thesis: verum
end;
 X is bounded_above
proof
take  r ; :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of X
let s be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not s in X or s <= r )
assume  s in X ; ::_thesis: s <= r
hence  s <= r by A1; ::_thesis: verum
end;
hence  r = upper_bound X by A1, A3, Def1; ::_thesis: verum
end;

registration
let X be non empty real-membered bounded_below set ;
identify lower_bound X with  inf X;
compatibility
 lower_bound X = inf X
proof
A1: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_X_holds_
s_>=_t_)_holds_
inf_X_>=_t
let t be real number ; ::_thesis: ( ( for s being real number st s in X holds
s >= t ) implies inf X >= t )
assume  for s being real number st s in X holds
s >= t ; ::_thesis: inf X >= t
then  for x being ext-real number st x in X holds
t <= x ;
then  t is LowerBound of X by XXREAL_2:def_2;
hence  inf X >= t by XXREAL_2:def_4; ::_thesis: verum
end;
 for s being real number st s in X holds
s >= inf X by XXREAL_2:3;
hence  lower_bound X = inf X by A1, Lm1; ::_thesis: verum
end;
end;

registration
let X be non empty real-membered bounded_above set ;
identify upper_bound X with  sup X;
compatibility
 upper_bound X = sup X
proof
A1: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_X_holds_
t_>=_s_)_holds_
t_>=_sup_X
let t be real number ; ::_thesis: ( ( for s being real number st s in X holds
t >= s ) implies t >= sup X )
assume  for s being real number st s in X holds
t >= s ; ::_thesis: t >= sup X
then  for x being ext-real number st x in X holds
x <= t ;
then  t is UpperBound of X by XXREAL_2:def_1;
hence  t >= sup X by XXREAL_2:def_3; ::_thesis: verum
end;
 for s being real number st s in X holds
s <= sup X by XXREAL_2:4;
hence  upper_bound X = sup X by A1, Lm2; ::_thesis: verum
end;
end;

definition
let X be Subset of REAL;
:: original: upper_bound
redefine func upper_bound X ->  Real;
coherence
 upper_bound X is Real by XREAL_0:def_1;
:: original: lower_bound
redefine func lower_bound X ->  Real;
coherence
 lower_bound X is Real by XREAL_0:def_1;
end;

theorem Th9: :: SEQ_4:9
for r being real number holds
( lower_bound {r} = r & upper_bound {r} = r ) by XXREAL_2:11, XXREAL_2:13;

theorem Th10: :: SEQ_4:10
for r being real number holds lower_bound {r} = upper_bound {r}
proof
let r be real number ; ::_thesis: lower_bound {r} = upper_bound {r}
 lower_bound {r} = r by XXREAL_2:13;
hence  lower_bound {r} = upper_bound {r} by XXREAL_2:11; ::_thesis: verum
end;

theorem :: SEQ_4:11
for X being Subset of REAL st X is real-bounded & not X is empty holds
lower_bound X <= upper_bound X
proof
let X be Subset of REAL; ::_thesis: ( X is real-bounded & not X is empty implies lower_bound X <= upper_bound X )
assume  ( X is real-bounded & not X is empty ) ; ::_thesis: lower_bound X <= upper_bound X
then reconsider X = X as non empty real-membered real-bounded set ;
 lower_bound X <= upper_bound X by XXREAL_2:40;
hence  lower_bound X <= upper_bound X ; ::_thesis: verum
end;

theorem :: SEQ_4:12
for X being Subset of REAL st X is real-bounded & not X is empty holds
( ex r, p being real number st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )
proof
let X be Subset of REAL; ::_thesis: ( X is real-bounded & not X is empty implies ( ex r, p being real number st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X ) )
assume that
A1: X is real-bounded and
A2: not X is empty ; ::_thesis: ( ex r, p being real number st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )
thus  ( ex r, p being real number st
( r in X & p in X & p <> r ) implies lower_bound X < upper_bound X ) ::_thesis: ( lower_bound X < upper_bound X implies ex r, p being real number st
( r in X & p in X & p <> r ) )
proof
given r, p being real number  such that A3: r in X and
A4: p in X and
A5: p <> r ; ::_thesis: lower_bound X < upper_bound X
A6: now__::_thesis:_(_r_<_p_implies_lower_bound_X_<_upper_bound_X_)
assume A7: r < p ; ::_thesis: lower_bound X < upper_bound X
 lower_bound X <= r by A1, A3, Def2;
then A8: lower_bound X < p by A7, XXREAL_0:2;
 p <= upper_bound X by A1, A4, Def1;
hence  lower_bound X < upper_bound X by A8, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_(_p_<_r_implies_lower_bound_X_<_upper_bound_X_)
assume A9: p < r ; ::_thesis: lower_bound X < upper_bound X
 lower_bound X <= p by A1, A4, Def2;
then A10: lower_bound X < r by A9, XXREAL_0:2;
 r <= upper_bound X by A1, A3, Def1;
hence  lower_bound X < upper_bound X by A10, XXREAL_0:2; ::_thesis: verum
end;
hence  lower_bound X < upper_bound X by A5, A6, XXREAL_0:1; ::_thesis: verum
end;
consider r being Element of REAL  such that
A11: r in X by A2, SUBSET_1:4;
assume that
A12: lower_bound X < upper_bound X and
A13: for r, p being real number st r in X & p in X holds
p = r ; ::_thesis: contradiction
 for x being set holds
( x in X iff x = r ) by A13, A11;
then  X = {r} by TARSKI:def_1;
hence  contradiction by A12, Th10; ::_thesis: verum
end;

theorem Th13: :: SEQ_4:13
for seq being Real_Sequence st seq is convergent holds
abs seq is convergent
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies abs seq is convergent )
assume  seq is convergent ; ::_thesis: abs seq is convergent
then consider g1 being real number  such that
A1: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by SEQ_2:def_6;
reconsider g1 = g1 as Real by XREAL_0:def_1;
take g = abs g1; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs (((abs seq) . b3) - g) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs (((abs seq) . b2) - g) ) )
assume  0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs (((abs seq) . b2) - g) )
then consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p by A1;
take n = n1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= abs (((abs seq) . b1) - g) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs (((abs seq) . m) - g) )
abs (g1 - (seq . m)) = abs (- ((seq . m) - g1))
.= abs ((seq . m) - g1) by COMPLEX1:52 ;
then  g - (abs (seq . m)) <= abs ((seq . m) - g1) by COMPLEX1:59;
then  ( (abs (seq . m)) - g <= abs ((seq . m) - g1) & - (abs ((seq . m) - g1)) <= - (g - (abs (seq . m))) ) by COMPLEX1:59, XREAL_1:24;
then  abs ((abs (seq . m)) - g) <= abs ((seq . m) - g1) by ABSVALUE:5;
then A3: abs (((abs seq) . m) - g) <= abs ((seq . m) - g1) by SEQ_1:12;
assume  n <= m ; ::_thesis: not p <= abs (((abs seq) . m) - g)
then  abs ((seq . m) - g1) < p by A2;
hence  not p <= abs (((abs seq) . m) - g) by A3, XXREAL_0:2; ::_thesis: verum
end;

registration
let seq be convergent Real_Sequence;
cluster|.seq.| ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = abs seq holds
b1 is convergent by Th13;
end;

theorem :: SEQ_4:14
for seq being Real_Sequence st seq is convergent holds
lim (abs seq) = abs (lim seq)
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies lim (abs seq) = abs (lim seq) )
assume A1: seq is convergent ; ::_thesis: lim (abs seq) = abs (lim seq)
now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((abs_seq)_._m)_-_(abs_(lim_seq)))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((abs seq) . m) - (abs (lim seq))) < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((abs seq) . m) - (abs (lim seq))) < p
then consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p by A1, SEQ_2:def_7;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
abs (((abs seq) . m) - (abs (lim seq))) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((abs seq) . m) - (abs (lim seq))) < p )
abs ((lim seq) - (seq . m)) = abs (- ((seq . m) - (lim seq)))
.= abs ((seq . m) - (lim seq)) by COMPLEX1:52 ;
then  (abs (lim seq)) - (abs (seq . m)) <= abs ((seq . m) - (lim seq)) by COMPLEX1:59;
then  ( (abs (seq . m)) - (abs (lim seq)) <= abs ((seq . m) - (lim seq)) & - (abs ((seq . m) - (lim seq))) <= - ((abs (lim seq)) - (abs (seq . m))) ) by COMPLEX1:59, XREAL_1:24;
then  abs ((abs (seq . m)) - (abs (lim seq))) <= abs ((seq . m) - (lim seq)) by ABSVALUE:5;
then A3: abs (((abs seq) . m) - (abs (lim seq))) <= abs ((seq . m) - (lim seq)) by SEQ_1:12;
assume  n <= m ; ::_thesis: abs (((abs seq) . m) - (abs (lim seq))) < p
then  abs ((seq . m) - (lim seq)) < p by A2;
hence  abs (((abs seq) . m) - (abs (lim seq))) < p by A3, XXREAL_0:2; ::_thesis: verum
end;
hence  lim (abs seq) = abs (lim seq) by A1, SEQ_2:def_7; ::_thesis: verum
end;

theorem :: SEQ_4:15
for seq being Real_Sequence st abs seq is convergent & lim (abs seq) = 0 holds
( seq is convergent & lim seq = 0 )
proof
let seq be Real_Sequence; ::_thesis: ( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) )
assume that
A1: abs seq is convergent and
A2: lim (abs seq) = 0 ; ::_thesis: ( seq is convergent & lim seq = 0 )
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(-_(abs_seq))_._n_<=_seq_._n_&_seq_._n_<=_(abs_seq)_._n_)
let n be Element of NAT ; ::_thesis: ( (- (abs seq)) . n <= seq . n & seq . n <= (abs seq) . n )
 - (abs (seq . n)) <= seq . n by ABSVALUE:4;
then A4: - ((abs seq) . n) <= seq . n by SEQ_1:12;
 seq . n <= abs (seq . n) by ABSVALUE:4;
hence  ( (- (abs seq)) . n <= seq . n & seq . n <= (abs seq) . n ) by A4, SEQ_1:10, SEQ_1:12; ::_thesis: verum
end;
A5: ( - (abs seq) is convergent & lim (- (abs seq)) = - (lim (abs seq)) ) by A1, SEQ_2:10;
hence  seq is convergent by A1, A2, A3, SEQ_2:19; ::_thesis: lim seq = 0
thus  lim seq = 0 by A1, A2, A5, A3, SEQ_2:20; ::_thesis: verum
end;

theorem Th16: :: SEQ_4:16
for seq1, seq being Real_Sequence st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent
proof
let seq1, seq be Real_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies seq1 is convergent )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; ::_thesis: seq1 is convergent
consider g1 being real number  such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by A2, SEQ_2:def_6;
take  g1 ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((seq1 . b3) - g1) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq1 . b2) - g1) ) )
assume  0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq1 . b2) - g1) )
then consider n1 being Element of NAT  such that
A4: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p by A3;
take n = n1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= abs ((seq1 . b1) - g1) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs ((seq1 . m) - g1) )
assume A5: n <= m ; ::_thesis: not p <= abs ((seq1 . m) - g1)
consider Nseq being V39() sequence of NAT such that
A6: seq1 = seq * Nseq by A1, VALUED_0:def_17;
 m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A5, XXREAL_0:2;
 seq1 . m = seq . (Nseq . m) by A6, FUNCT_2:15;
hence  not p <= abs ((seq1 . m) - g1) by A4, A7; ::_thesis: verum
end;

theorem Th17: :: SEQ_4:17
for seq1, seq being Real_Sequence st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof
let seq1, seq be Real_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; ::_thesis: lim seq1 = lim seq
consider Nseq being V39() sequence of NAT such that
A3: seq1 = seq * Nseq by A1, VALUED_0:def_17;
A4: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq1_._m)_-_(lim_seq))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
then consider n1 being Element of NAT  such that
A5: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p by A2, SEQ_2:def_7;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq1 . m) - (lim seq)) < p )
assume A6: n <= m ; ::_thesis: abs ((seq1 . m) - (lim seq)) < p
 m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A6, XXREAL_0:2;
 seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15;
hence  abs ((seq1 . m) - (lim seq)) < p by A5, A7; ::_thesis: verum
end;
 seq1 is convergent by A1, A2, Th16;
hence  lim seq1 = lim seq by A4, SEQ_2:def_7; ::_thesis: verum
end;

theorem Th18: :: SEQ_4:18
for seq, seq1 being Real_Sequence st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n ; ::_thesis: seq1 is convergent
consider g1 being real number  such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by A1, SEQ_2:def_6;
consider k being Element of NAT  such that
A4: for n being Element of NAT st k <= n holds
seq1 . n = seq . n by A2;
take g = g1; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((seq1 . b3) - g) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq1 . b2) - g) ) )
assume  0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq1 . b2) - g) )
then consider n1 being Element of NAT  such that
A5: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p by A3;
A6: now__::_thesis:_(_n1_<=_k_implies_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq1_._m)_-_g)_<_p_)
assume A7: n1 <= k ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g) < p
take n = k; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq1 . m) - g) < p )
assume A8: n <= m ; ::_thesis: abs ((seq1 . m) - g) < p
then  n1 <= m by A7, XXREAL_0:2;
then  abs ((seq . m) - g1) < p by A5;
hence  abs ((seq1 . m) - g) < p by A4, A8; ::_thesis: verum
end;
now__::_thesis:_(_k_<=_n1_implies_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq1_._m)_-_g)_<_p_)
assume A9: k <= n1 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g) < p
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq1 . m) - g) < p )
assume A10: n <= m ; ::_thesis: abs ((seq1 . m) - g) < p
then  seq1 . m = seq . m by A4, A9, XXREAL_0:2;
hence  abs ((seq1 . m) - g) < p by A5, A10; ::_thesis: verum
end;
hence  ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq1 . b2) - g) ) by A6; ::_thesis: verum
end;

theorem :: SEQ_4:19
for seq, seq1 being Real_Sequence st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
lim seq = lim seq1
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n implies lim seq = lim seq1 )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n ; ::_thesis: lim seq = lim seq1
consider k being Element of NAT  such that
A3: for n being Element of NAT st k <= n holds
seq1 . n = seq . n by A2;
A4: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq1_._m)_-_(lim_seq))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
then consider n1 being Element of NAT  such that
A5: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p by A1, SEQ_2:def_7;
A6: now__::_thesis:_(_n1_<=_k_implies_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq1_._m)_-_(lim_seq))_<_p_)
assume A7: n1 <= k ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
take n = k; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq1 . m) - (lim seq)) < p )
assume A8: n <= m ; ::_thesis: abs ((seq1 . m) - (lim seq)) < p
then  n1 <= m by A7, XXREAL_0:2;
then  abs ((seq . m) - (lim seq)) < p by A5;
hence  abs ((seq1 . m) - (lim seq)) < p by A3, A8; ::_thesis: verum
end;
now__::_thesis:_(_k_<=_n1_implies_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq1_._m)_-_(lim_seq))_<_p_)
assume A9: k <= n1 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq1 . m) - (lim seq)) < p )
assume A10: n <= m ; ::_thesis: abs ((seq1 . m) - (lim seq)) < p
then  seq1 . m = seq . m by A3, A9, XXREAL_0:2;
hence  abs ((seq1 . m) - (lim seq)) < p by A5, A10; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p by A6; ::_thesis: verum
end;
 seq1 is convergent by A1, A2, Th18;
hence  lim seq = lim seq1 by A4, SEQ_2:def_7; ::_thesis: verum
end;

registration
cluster Function-like constant V18( NAT , REAL )  ->  convergent for Element of bool [:NAT,REAL:];
coherence
 for b1 being Real_Sequence st b1 is constant holds
b1 is convergent ;
end;

registration
cluster Relation-like NAT -defined REAL -valued Function-like constant non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued for Element of bool [:NAT,REAL:];
existence
 ex b1 being Real_Sequence st b1 is constant
proof
take  the constant Real_Sequence ; ::_thesis: the constant Real_Sequence is constant
thus  the constant Real_Sequence is constant ; ::_thesis: verum
end;
end;

registration
let seq be convergent Real_Sequence;
let k be Element of NAT ;
clusterseq ^\ k ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = seq ^\ k holds
b1 is convergent by Th16;
end;

theorem :: SEQ_4:20
for k being Element of NAT
for seq being Real_Sequence st seq is convergent holds
lim (seq ^\ k) = lim seq by Th17;

theorem Th21: :: SEQ_4:21
for k being Element of NAT
for seq being Real_Sequence st seq ^\ k is convergent holds
seq is convergent
proof
let k be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq ^\ k is convergent holds
seq is convergent
let seq be Real_Sequence; ::_thesis: ( seq ^\ k is convergent implies seq is convergent )
assume  seq ^\ k is convergent ; ::_thesis: seq is convergent
then consider g1 being real number  such that
A1: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ^\ k) . m) - g1) < p by SEQ_2:def_6;
take  g1 ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((seq . b3) - g1) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq . b2) - g1) ) )
assume  0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq . b2) - g1) )
then consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
abs (((seq ^\ k) . m) - g1) < p by A1;
take n = n1 + k; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= abs ((seq . b1) - g1) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs ((seq . m) - g1) )
assume A3: n <= m ; ::_thesis: not p <= abs ((seq . m) - g1)
then consider l being Nat such that
A4: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
 m - k = ((n1 + l) + k) + (- k) by A4;
then consider m1 being Element of NAT  such that
A5: m1 = m - k ;
now__::_thesis:_n1_<=_m1
assume  not n1 <= m1 ; ::_thesis: contradiction
then  m1 + k < n1 + k by XREAL_1:6;
hence  contradiction by A3, A5; ::_thesis: verum
end;
then A6: abs (((seq ^\ k) . m1) - g1) < p by A2;
 m1 + k = m by A5;
hence  not p <= abs ((seq . m) - g1) by A6, NAT_1:def_3; ::_thesis: verum
end;

theorem :: SEQ_4:22
for k being Element of NAT
for seq being Real_Sequence st seq ^\ k is convergent holds
lim seq = lim (seq ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq ^\ k is convergent holds
lim seq = lim (seq ^\ k)
let seq be Real_Sequence; ::_thesis: ( seq ^\ k is convergent implies lim seq = lim (seq ^\ k) )
assume A1: seq ^\ k is convergent ; ::_thesis: lim seq = lim (seq ^\ k)
A2: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq_._m)_-_(lim_(seq_^\_k)))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (lim (seq ^\ k))) < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (lim (seq ^\ k))) < p
then consider n1 being Element of NAT  such that
A3: for m being Element of NAT st n1 <= m holds
abs (((seq ^\ k) . m) - (lim (seq ^\ k))) < p by A1, SEQ_2:def_7;
take n = n1 + k; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - (lim (seq ^\ k))) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - (lim (seq ^\ k))) < p )
assume A4: n <= m ; ::_thesis: abs ((seq . m) - (lim (seq ^\ k))) < p
then consider l being Nat such that
A5: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
 m - k = ((n1 + l) + k) + (- k) by A5;
then consider m1 being Element of NAT  such that
A6: m1 = m - k ;
now__::_thesis:_n1_<=_m1
assume  not n1 <= m1 ; ::_thesis: contradiction
then  m1 + k < n1 + k by XREAL_1:6;
hence  contradiction by A4, A6; ::_thesis: verum
end;
then A7: abs (((seq ^\ k) . m1) - (lim (seq ^\ k))) < p by A3;
 m1 + k = m by A6;
hence  abs ((seq . m) - (lim (seq ^\ k))) < p by A7, NAT_1:def_3; ::_thesis: verum
end;
 seq is convergent by A1, Th21;
hence  lim seq = lim (seq ^\ k) by A2, SEQ_2:def_7; ::_thesis: verum
end;

theorem Th23: :: SEQ_4:23
for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Element of NAT st seq ^\ k is non-zero
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies ex k being Element of NAT st seq ^\ k is non-zero )
assume that
A1: seq is convergent and
A2: lim seq <> 0 ; ::_thesis: ex k being Element of NAT st seq ^\ k is non-zero
consider n1 being Element of NAT  such that
A3: for m being Element of NAT st n1 <= m holds
(abs (lim seq)) / 2 < abs (seq . m) by A1, A2, SEQ_2:16;
take k = n1; ::_thesis: seq ^\ k is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_^\_k)_._n_<>_0
let n be Element of NAT ; ::_thesis: (seq ^\ k) . n <> 0
 0 + k <= n + k by XREAL_1:7;
then  (abs (lim seq)) / 2 < abs (seq . (n + k)) by A3;
then A4: (abs (lim seq)) / 2 < abs ((seq ^\ k) . n) by NAT_1:def_3;
 0 < abs (lim seq) by A2, COMPLEX1:47;
then  0 / 2 < (abs (lim seq)) / 2 by XREAL_1:74;
hence  (seq ^\ k) . n <> 0 by A4, ABSVALUE:2; ::_thesis: verum
end;
hence  seq ^\ k is non-zero by SEQ_1:5; ::_thesis: verum
end;

theorem :: SEQ_4:24
for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero )
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero ) )
assume  ( seq is convergent & lim seq <> 0 ) ; ::_thesis: ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero )
then consider k being Element of NAT  such that
A1: seq ^\ k is non-zero by Th23;
take  seq ^\ k ; ::_thesis: ( seq ^\ k is subsequence of seq & seq ^\ k is non-zero )
thus  ( seq ^\ k is subsequence of seq & seq ^\ k is non-zero ) by A1; ::_thesis: verum
end;

theorem Th25: :: SEQ_4:25
for r being real number
for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Element of NAT st seq . n = r ) holds
lim seq = r
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Element of NAT st seq . n = r ) holds
lim seq = r
let seq be Real_Sequence; ::_thesis: ( seq is constant & ( r in rng seq or ex n being Element of NAT st seq . n = r ) implies lim seq = r )
assume A1: seq is constant ; ::_thesis: ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r )
then consider r1 being Real such that
A2: rng seq = {r1} by FUNCT_2:111;
A3: now__::_thesis:_(_r_in_rng_seq_&_(_r_in_rng_seq_or_ex_n_being_Element_of_NAT_st_seq_._n_=_r_)_implies_lim_seq_=_r_)
assume A4: r in rng seq ; ::_thesis: ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r )
consider r2 being Real such that
A5: for n being Nat holds seq . n = r2 by A1, VALUED_0:def_18;
A6: r = r1 by A4, A2, TARSKI:def_1;
now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq_._m)_-_r)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p )
assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - r) < p )
assume  n <= m ; ::_thesis: abs ((seq . m) - r) < p
 m in NAT ;
then  m in dom seq by FUNCT_2:def_1;
then  seq . m in rng seq by FUNCT_1:def_3;
then  r2 in rng seq by A5;
then  r2 = r by A2, A6, TARSKI:def_1;
then  seq . m = r by A5;
hence  abs ((seq . m) - r) < p by A7, ABSVALUE:2; ::_thesis: verum
end;
hence  ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r ) by A1, SEQ_2:def_7; ::_thesis: verum
end;
A8: now__::_thesis:_(_ex_n_being_Element_of_NAT_st_seq_._n_=_r_&_(_r_in_rng_seq_or_ex_n_being_Element_of_NAT_st_seq_._n_=_r_)_implies_lim_seq_=_r_)
assume A9: ex n being Element of NAT st seq . n = r ; ::_thesis: ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r )
consider n being Element of NAT  such that
A10: seq . n = r by A9;
 n in NAT ;
then  n in dom seq by FUNCT_2:def_1;
hence  ( ( not r in rng seq & ( for n being Element of NAT holds not seq . n = r ) ) or lim seq = r ) by A3, A10, FUNCT_1:def_3; ::_thesis: verum
end;
assume  ( r in rng seq or ex n being Element of NAT st seq . n = r ) ; ::_thesis: lim seq = r
hence  lim seq = r by A3, A8; ::_thesis: verum
end;

theorem :: SEQ_4:26
for seq being Real_Sequence st seq is constant holds
for n being Element of NAT holds lim seq = seq . n by Th25;

theorem :: SEQ_4:27
for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
for seq1 being Real_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 ") = (lim seq) "
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies for seq1 being Real_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 ") = (lim seq) " )
assume that
A1: seq is convergent and
A2: lim seq <> 0 ; ::_thesis: for seq1 being Real_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 ") = (lim seq) "
let seq1 be Real_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq1 is non-zero implies lim (seq1 ") = (lim seq) " )
assume that
A3: seq1 is subsequence of seq and
A4: seq1 is non-zero ; ::_thesis: lim (seq1 ") = (lim seq) "
 lim seq1 = lim seq by A1, A3, Th17;
hence  lim (seq1 ") = (lim seq) " by A1, A2, A3, A4, Th16, SEQ_2:22; ::_thesis: verum
end;

theorem Th28: :: SEQ_4:28
for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
seq is convergent
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
seq is convergent
let seq be Real_Sequence; ::_thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) implies seq is convergent )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = 1 / (n + r) ; ::_thesis: seq is convergent
take  0 ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((seq . b3) - 0) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq . b2) - 0) ) )
assume A3: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq . b2) - 0) )
consider k1 being Element of NAT  such that
A4: p " < k1 by Th3;
 (p ") + 0 < k1 + r by A1, A4, XREAL_1:8;
then  1 / (k1 + r) < 1 / (p ") by A3, XREAL_1:76;
then A5: 1 / (k1 + r) < 1 * ((p ") ") by XCMPLX_0:def_9;
take n = k1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= abs ((seq . b1) - 0) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs ((seq . m) - 0) )
assume  n <= m ; ::_thesis: not p <= abs ((seq . m) - 0)
then A6: n + r <= m + r by XREAL_1:6;
 0 < p " by A3;
then  1 / (m + r) <= 1 / (n + r) by A1, A4, A6, XREAL_1:118;
then A7: 1 / (m + r) < p by A5, XXREAL_0:2;
 seq . m = 1 / (m + r) by A2;
hence  not p <= abs ((seq . m) - 0) by A1, A7, ABSVALUE:def_1; ::_thesis: verum
end;

theorem Th29: :: SEQ_4:29
for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
lim seq = 0
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
lim seq = 0
let seq be Real_Sequence; ::_thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) implies lim seq = 0 )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = 1 / (n + r) ; ::_thesis: lim seq = 0
A3: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq_._m)_-_0)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p )
assume A4: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p
consider k1 being Element of NAT  such that
A5: p " < k1 by Th3;
 (p ") + 0 < k1 + r by A1, A5, XREAL_1:8;
then  1 / (k1 + r) < 1 / (p ") by A4, XREAL_1:76;
then A6: 1 / (k1 + r) < 1 * ((p ") ") by XCMPLX_0:def_9;
take n = k1; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - 0) < p )
assume  n <= m ; ::_thesis: abs ((seq . m) - 0) < p
then A7: n + r <= m + r by XREAL_1:6;
 0 < p " by A4;
then  1 / (m + r) <= 1 / (n + r) by A1, A5, A7, XREAL_1:118;
then A8: 1 / (m + r) < p by A6, XXREAL_0:2;
 ( seq . m = 1 / (m + r) & 0 <= m ) by A2;
hence  abs ((seq . m) - 0) < p by A1, A8, ABSVALUE:def_1; ::_thesis: verum
end;
 seq is convergent by A1, A2, Th28;
hence  lim seq = 0 by A3, SEQ_2:def_7; ::_thesis: verum
end;

theorem :: SEQ_4:30
for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = 1 / (n + 1) ) holds
( seq is convergent & lim seq = 0 ) by Th28, Th29;

theorem :: SEQ_4:31
for r, g being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / (n + r) ) holds
( seq is convergent & lim seq = 0 )
proof
let r, g be real number ; ::_thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / (n + r) ) holds
( seq is convergent & lim seq = 0 )
let seq be Real_Sequence; ::_thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = g / (n + r) ) implies ( seq is convergent & lim seq = 0 ) )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = g / (n + r) ; ::_thesis: ( seq is convergent & lim seq = 0 )
reconsider r1 = r as Real by XREAL_0:def_1;
deffunc H1( Element of NAT ) ->  Element of REAL = 1 / ($1 + r1);
consider seq1 being Real_Sequence such that
A3: for n being Element of NAT holds seq1 . n = H1(n) from SEQ_1:sch_1();
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(g_(#)_seq1)_._n_=_seq_._n
let n be Element of NAT ; ::_thesis: (g (#) seq1) . n = seq . n
thus (g (#) seq1) . n = g * (seq1 . n) by SEQ_1:9
.= g * (1 / (n + r)) by A3
.= g * (1 * ((n + r) ")) by XCMPLX_0:def_9
.= g / (n + r) by XCMPLX_0:def_9
.= seq . n by A2 ; ::_thesis: verum
end;
A5: g (#) seq1 is convergent by A1, A3, Th28, SEQ_2:7;
lim (g (#) seq1) = g * (lim seq1) by A1, A3, Th28, SEQ_2:8
.= g * 0 by A1, A3, Th29
.= 0 ;
hence  ( seq is convergent & lim seq = 0 ) by A5, A4, FUNCT_2:63; ::_thesis: verum
end;

theorem Th32: :: SEQ_4:32
for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
seq is convergent
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
seq is convergent
let seq be Real_Sequence; ::_thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) implies seq is convergent )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ; ::_thesis: seq is convergent
take  0 ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((seq . b3) - 0) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq . b2) - 0) ) )
consider k1 being Element of NAT  such that
A3: p " < k1 by Th3;
assume A4: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs ((seq . b2) - 0) )
then A5: k1 > 0 by A3;
then  k1 >= 1 + 0 by NAT_1:13;
then  k1 <= k1 * k1 by XREAL_1:151;
then A6: k1 + r <= (k1 * k1) + r by XREAL_1:6;
take n = k1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= abs ((seq . b1) - 0) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs ((seq . m) - 0) )
assume A7: n <= m ; ::_thesis: not p <= abs ((seq . m) - 0)
 n * n <= m * m by A7, XREAL_1:66;
then A8: (n * n) + r <= (m * m) + r by XREAL_1:6;
 (p ") + 0 < k1 + r by A1, A3, XREAL_1:8;
then  (p ") + 0 < (k1 * k1) + r by A6, XXREAL_0:2;
then  1 / ((k1 * k1) + r) < 1 / (p ") by A4, XREAL_1:76;
then A9: 1 / ((k1 * k1) + r) < 1 * ((p ") ") by XCMPLX_0:def_9;
 0 < n ^2 by A5, SQUARE_1:12;
then  1 / ((m * m) + r) <= 1 / ((n * n) + r) by A1, A8, XREAL_1:118;
then A10: 1 / ((m * m) + r) < p by A9, XXREAL_0:2;
 seq . m = 1 / ((m * m) + r) by A2;
hence  not p <= abs ((seq . m) - 0) by A1, A10, ABSVALUE:def_1; ::_thesis: verum
end;

theorem Th33: :: SEQ_4:33
for r being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0
let seq be Real_Sequence; ::_thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) implies lim seq = 0 )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ; ::_thesis: lim seq = 0
A3: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq_._m)_-_0)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p )
consider k1 being Element of NAT  such that
A4: p " < k1 by Th3;
assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p
then A6: k1 > 0 by A4;
then  k1 >= 1 + 0 by NAT_1:13;
then  k1 <= k1 * k1 by XREAL_1:151;
then A7: k1 + r <= (k1 * k1) + r by XREAL_1:6;
take n = k1; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - 0) < p )
assume  n <= m ; ::_thesis: abs ((seq . m) - 0) < p
then  n * n <= m * m by XREAL_1:66;
then A8: (n * n) + r <= (m * m) + r by XREAL_1:6;
 (p ") + 0 < k1 + r by A1, A4, XREAL_1:8;
then  (p ") + 0 < (k1 * k1) + r by A7, XXREAL_0:2;
then  1 / ((k1 * k1) + r) < 1 / (p ") by A5, XREAL_1:76;
then A9: 1 / ((k1 * k1) + r) < 1 * ((p ") ") by XCMPLX_0:def_9;
 0 < n ^2 by A6, SQUARE_1:12;
then  1 / ((m * m) + r) <= 1 / ((n * n) + r) by A1, A8, XREAL_1:118;
then A10: 1 / ((m * m) + r) < p by A9, XXREAL_0:2;
 ( seq . m = 1 / ((m * m) + r) & 0 <= m * m ) by A2;
hence  abs ((seq . m) - 0) < p by A1, A10, ABSVALUE:def_1; ::_thesis: verum
end;
 seq is convergent by A1, A2, Th32;
hence  lim seq = 0 by A3, SEQ_2:def_7; ::_thesis: verum
end;

theorem :: SEQ_4:34
for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = 1 / ((n * n) + 1) ) holds
( seq is convergent & lim seq = 0 ) by Th32, Th33;

theorem :: SEQ_4:35
for r, g being real number
for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / ((n * n) + r) ) holds
( seq is convergent & lim seq = 0 )
proof
let r, g be real number ; ::_thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / ((n * n) + r) ) holds
( seq is convergent & lim seq = 0 )
let seq be Real_Sequence; ::_thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = g / ((n * n) + r) ) implies ( seq is convergent & lim seq = 0 ) )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = g / ((n * n) + r) ; ::_thesis: ( seq is convergent & lim seq = 0 )
reconsider r1 = r as Real by XREAL_0:def_1;
deffunc H1( Element of NAT ) ->  Element of REAL = 1 / (($1 * $1) + r1);
consider seq1 being Real_Sequence such that
A3: for n being Element of NAT holds seq1 . n = H1(n) from SEQ_1:sch_1();
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(g_(#)_seq1)_._n_=_seq_._n
let n be Element of NAT ; ::_thesis: (g (#) seq1) . n = seq . n
thus (g (#) seq1) . n = g * (seq1 . n) by SEQ_1:9
.= g * (1 / ((n * n) + r)) by A3
.= g * (1 * (((n * n) + r) ")) by XCMPLX_0:def_9
.= g / ((n * n) + r) by XCMPLX_0:def_9
.= seq . n by A2 ; ::_thesis: verum
end;
A5: g (#) seq1 is convergent by A1, A3, Th32, SEQ_2:7;
lim (g (#) seq1) = g * (lim seq1) by A1, A3, Th32, SEQ_2:8
.= g * 0 by A1, A3, Th33
.= 0 ;
hence  ( seq is convergent & lim seq = 0 ) by A5, A4, FUNCT_2:63; ::_thesis: verum
end;

registration
cluster Function-like V18( NAT , REAL ) V41() bounded_above  ->  convergent for Element of bool [:NAT,REAL:];
coherence
 for b1 being Real_Sequence st b1 is V41() & b1 is bounded_above holds
b1 is convergent
proof
let seq be Real_Sequence; ::_thesis: ( seq is V41() & seq is bounded_above implies seq is convergent )
assume that
A1: seq is V41() and
A2: seq is bounded_above ; ::_thesis: seq is convergent
consider r2 being real number  such that
A3: for n being Element of NAT holds seq . n < r2 by A2, SEQ_2:def_3;
defpred S1[ Real] means  ex n being Element of NAT st c1 = seq . n;
consider X being Subset of REAL such that
A4: for p being Real holds
( p in X iff S1[p] ) from SUBSET_1:sch_3();
A5: now__::_thesis:_ex_r_being_real_number_st_
for_p_being_real_number_st_p_in_X_holds_
p_<=_r
take r = r2; ::_thesis: for p being real number st p in X holds
p <= r
let p be real number ; ::_thesis: ( p in X implies p <= r )
assume  p in X ; ::_thesis: p <= r
then  ex n1 being Element of NAT st p = seq . n1 by A4;
hence  p <= r by A3; ::_thesis: verum
end;
A6: ( ex r being real number st
for p being real number st p in X holds
p <= r implies X is bounded_above )
proof
given r being real number  such that A7: for p being real number st p in X holds
p <= r ; ::_thesis: X is bounded_above
take  r ; :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of X
let p be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not p in X or p <= r )
thus  ( not p in X or p <= r ) by A7; ::_thesis: verum
end;
take g = upper_bound X; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((seq . b3) - g) ) )
let s be real number ; ::_thesis: ( s <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not s <= abs ((seq . b2) - g) ) )
assume A8: 0 < s ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not s <= abs ((seq . b2) - g) )
 seq . 0 in X by A4;
then consider p1 being real number  such that
A9: p1 in X and
A10: (upper_bound X) - s < p1 by A6, A8, Def1;
consider n1 being Element of NAT  such that
A11: p1 = seq . n1 by A4, A9;
take n = n1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not s <= abs ((seq . b1) - g) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not s <= abs ((seq . m) - g) )
assume  n <= m ; ::_thesis: not s <= abs ((seq . m) - g)
then  seq . n <= seq . m by A1, SEQM_3:6;
then  g + (- s) < seq . m by A10, A11, XXREAL_0:2;
then A12: - s < (seq . m) - g by XREAL_1:20;
 seq . m in X by A4;
then  seq . m <= g by A6, A5, Def1;
then  (seq . m) + 0 < g + s by A8, XREAL_1:8;
then  (seq . m) - g < s by XREAL_1:19;
hence  not s <= abs ((seq . m) - g) by A12, SEQ_2:1; ::_thesis: verum
end;
end;

registration
cluster Function-like V18( NAT , REAL ) V42() bounded_below  ->  convergent for Element of bool [:NAT,REAL:];
coherence
 for b1 being Real_Sequence st b1 is V42() & b1 is bounded_below holds
b1 is convergent
proof
let seq be Real_Sequence; ::_thesis: ( seq is V42() & seq is bounded_below implies seq is convergent )
assume that
A1: seq is V42() and
A2: seq is bounded_below ; ::_thesis: seq is convergent
defpred S1[ Real] means  ex n being Element of NAT st c1 = seq . n;
consider X being Subset of REAL such that
A3: for p being Real holds
( p in X iff S1[p] ) from SUBSET_1:sch_3();
take g = lower_bound X; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((seq . b3) - g) ) )
let s be real number ; ::_thesis: ( s <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not s <= abs ((seq . b2) - g) ) )
assume A4: 0 < s ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not s <= abs ((seq . b2) - g) )
A5: ( ex r being real number st
for p being real number st p in X holds
r <= p implies X is bounded_below )
proof
given r being real number  such that A6: for p being real number st p in X holds
r <= p ; ::_thesis: X is bounded_below
take  r ; :: according to XXREAL_2:def_9 ::_thesis: r is LowerBound of X
let p be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not p in X or r <= p )
thus  ( not p in X or r <= p ) by A6; ::_thesis: verum
end;
 seq . 0 in X by A3;
then consider p1 being real number  such that
A7: p1 in X and
A8: p1 < (lower_bound X) + s by A5, A4, Def2;
consider n1 being Element of NAT  such that
A9: p1 = seq . n1 by A3, A7;
take n = n1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not s <= abs ((seq . b1) - g) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not s <= abs ((seq . m) - g) )
consider r1 being real number  such that
A10: for n being Element of NAT holds r1 < seq . n by A2, SEQ_2:def_4;
A11: now__::_thesis:_ex_r_being_real_number_st_
for_p_being_real_number_st_p_in_X_holds_
r_<=_p
take r = r1; ::_thesis: for p being real number st p in X holds
r <= p
let p be real number ; ::_thesis: ( p in X implies r <= p )
assume  p in X ; ::_thesis: r <= p
then  ex n1 being Element of NAT st p = seq . n1 by A3;
hence  r <= p by A10; ::_thesis: verum
end;
 seq . m in X by A3;
then  0 + g <= seq . m by A5, A11, Def2;
then A12: 0 <= (seq . m) - g by XREAL_1:19;
assume  n <= m ; ::_thesis: not s <= abs ((seq . m) - g)
then  seq . m <= seq . n by A1, SEQM_3:8;
then  seq . m < g + s by A8, A9, XXREAL_0:2;
then A13: (seq . m) - g < s by XREAL_1:19;
 - s < - 0 by A4, XREAL_1:24;
hence  not s <= abs ((seq . m) - g) by A13, A12, SEQ_2:1; ::_thesis: verum
end;
end;

registration
cluster Function-like V18( NAT , REAL ) monotone bounded  ->  convergent for Element of bool [:NAT,REAL:];
coherence
 for b1 being Real_Sequence st b1 is monotone & b1 is bounded holds
b1 is convergent
proof
let seq be Real_Sequence; ::_thesis: ( seq is monotone & seq is bounded implies seq is convergent )
assume that
A1: seq is monotone and
A2: seq is bounded ; ::_thesis: seq is convergent
A3: ( seq is V42() implies seq is convergent ) by A2;
 ( seq is V41() implies seq is convergent ) by A2;
hence  seq is convergent by A1, A3, SEQM_3:def_5; ::_thesis: verum
end;
end;

theorem Th36: :: SEQ_4:36
for seq being Real_Sequence st seq is monotone & seq is bounded holds
seq is convergent ;

theorem :: SEQ_4:37
for seq being Real_Sequence st seq is bounded_above & seq is V41() holds
for n being Element of NAT holds seq . n <= lim seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded_above & seq is V41() implies for n being Element of NAT holds seq . n <= lim seq )
assume that
A1: seq is bounded_above and
A2: seq is V41() ; ::_thesis: for n being Element of NAT holds seq . n <= lim seq
let m be Element of NAT ; ::_thesis: seq . m <= lim seq
set seq1 = NAT --> (seq . m);
deffunc H1( Nat) ->  Element of REAL = seq . ($1 + m);
consider seq2 being Real_Sequence such that
A3: for n being Element of NAT holds seq2 . n = H1(n) from SEQ_1:sch_1();
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(NAT_-->_(seq_._m))_._n_<=_seq2_._n
let n be Element of NAT ; ::_thesis: (NAT --> (seq . m)) . n <= seq2 . n
 ( (NAT --> (seq . m)) . n = seq . m & seq2 . n = seq . (m + n) ) by A3, FUNCOP_1:7;
hence  (NAT --> (seq . m)) . n <= seq2 . n by A2, SEQM_3:5; ::_thesis: verum
end;
 (NAT --> (seq . m)) . 0 = seq . m by FUNCOP_1:7;
then A5: lim (NAT --> (seq . m)) = seq . m by Th25;
now__::_thesis:_for_n_being_Nat_holds_seq2_._n_=_H1(n)
let n be Nat; ::_thesis: seq2 . n = H1(n)
 n in NAT by ORDINAL1:def_12;
hence  seq2 . n = H1(n) by A3; ::_thesis: verum
end;
then A6: seq2 = seq ^\ m by NAT_1:def_3;
then  lim seq2 = lim seq by A1, A2, Th17;
hence  seq . m <= lim seq by A1, A2, A5, A6, A4, SEQ_2:18; ::_thesis: verum
end;

theorem :: SEQ_4:38
for seq being Real_Sequence st seq is bounded_below & seq is V42() holds
for n being Element of NAT holds lim seq <= seq . n
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded_below & seq is V42() implies for n being Element of NAT holds lim seq <= seq . n )
assume that
A1: seq is bounded_below and
A2: seq is V42() ; ::_thesis: for n being Element of NAT holds lim seq <= seq . n
let m be Element of NAT ; ::_thesis: lim seq <= seq . m
set seq1 = NAT --> (seq . m);
deffunc H1( Nat) ->  Element of REAL = seq . ($1 + m);
consider seq2 being Real_Sequence such that
A3: for n being Element of NAT holds seq2 . n = H1(n) from SEQ_1:sch_1();
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq2_._n_<=_(NAT_-->_(seq_._m))_._n
let n be Element of NAT ; ::_thesis: seq2 . n <= (NAT --> (seq . m)) . n
 ( (NAT --> (seq . m)) . n = seq . m & seq2 . n = seq . (m + n) ) by A3, FUNCOP_1:7;
hence  seq2 . n <= (NAT --> (seq . m)) . n by A2, SEQM_3:7; ::_thesis: verum
end;
 (NAT --> (seq . m)) . 0 = seq . m by FUNCOP_1:7;
then A5: lim (NAT --> (seq . m)) = seq . m by Th25;
now__::_thesis:_for_n_being_Nat_holds_seq2_._n_=_H1(n)
let n be Nat; ::_thesis: seq2 . n = H1(n)
 n in NAT by ORDINAL1:def_12;
hence  seq2 . n = H1(n) by A3; ::_thesis: verum
end;
then A6: seq2 = seq ^\ m by NAT_1:def_3;
then  lim seq2 = lim seq by A1, A2, Th17;
hence  lim seq <= seq . m by A1, A2, A5, A6, A4, SEQ_2:18; ::_thesis: verum
end;

theorem Th39: :: SEQ_4:39
for seq being Real_Sequence ex Nseq being V39() sequence of NAT st seq * Nseq is monotone
proof
let seq be Real_Sequence; ::_thesis: ex Nseq being V39() sequence of NAT st seq * Nseq is monotone
defpred S1[ Element of NAT ] means  for m being Element of NAT st $1 < m holds
seq . $1 < seq . m;
consider XN being Subset of NAT such that
A1: for n being Element of NAT holds
( n in XN iff S1[n] ) from SUBSET_1:sch_3();
A2: now__::_thesis:_(_ex_k1_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_in_XN_holds_
n_<=_k1_implies_ex_Nseq1_being_V39()_sequence_of_NAT_st_seq_*_Nseq1_is_monotone_)
given k1 being Element of NAT  such that A3: for n being Element of NAT st n in XN holds
n <= k1 ; ::_thesis: ex Nseq1 being V39() sequence of NAT st seq * Nseq1 is monotone
set seq1 = seq ^\ (1 + k1);
defpred S2[ set , set , set ] means  for k, l being Element of NAT st k = $2 & l = $3 holds
( k < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k & ( for m being Element of NAT st k < m & (seq ^\ (1 + k1)) . m <= (seq ^\ (1 + k1)) . k holds
l <= m ) );
A4: now__::_thesis:_for_k_being_Element_of_NAT_st_k1_<_k_holds_
ex_n_being_Element_of_NAT_st_
(_k_<_n_&_seq_._n_<=_seq_._k_)
let k be Element of NAT ; ::_thesis: ( k1 < k implies ex n being Element of NAT st
( k < n & seq . n <= seq . k ) )
assume  k1 < k ; ::_thesis: ex n being Element of NAT st
( k < n & seq . n <= seq . k )
then  not k in XN by A3;
then consider m being Element of NAT  such that
A5: k < m and
A6: not seq . k < seq . m by A1;
take n = m; ::_thesis: ( k < n & seq . n <= seq . k )
thus  k < n by A5; ::_thesis: seq . n <= seq . k
thus  seq . n <= seq . k by A6; ::_thesis: verum
end;
A7: now__::_thesis:_for_k_being_Element_of_NAT_ex_l_being_Element_of_NAT_st_
(_k_<_l_&_(seq_^\_(1_+_k1))_._l_<=_(seq_^\_(1_+_k1))_._k_)
let k be Element of NAT ; ::_thesis: ex l being Element of NAT st
( k < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k )
 0 + k1 < (k + 1) + k1 by XREAL_1:8;
then consider n being Element of NAT  such that
A8: (k + 1) + k1 < n and
A9: seq . n <= seq . ((k + 1) + k1) by A4;
consider m being Nat such that
A10: n = ((k + 1) + k1) + m by A8, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
 n - (1 + k1) = (k + 0) + m by A10;
then consider n1 being Element of NAT  such that
A11: n1 = n - (1 + k1) ;
 seq . n <= seq . (k + (1 + k1)) by A9;
then A12: seq . n <= (seq ^\ (1 + k1)) . k by NAT_1:def_3;
take l = n1; ::_thesis: ( k < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k )
now__::_thesis:_k_<_l
assume  not k < l ; ::_thesis: contradiction
then  (n - (1 + k1)) + (1 + k1) <= k + (1 + k1) by A11, XREAL_1:6;
hence  contradiction by A8; ::_thesis: verum
end;
hence  k < l ; ::_thesis: (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k
 n = l + (1 + k1) by A11;
hence  (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k by A12, NAT_1:def_3; ::_thesis: verum
end;
A13: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S2[n,x,y]
defpred S3[ Nat] means ( x < $1 & (seq ^\ (1 + k1)) . $1 <= (seq ^\ (1 + k1)) . x );
 ex n being Element of NAT st S3[n] by A7;
then A14: ex n being Nat st S3[n] ;
 ex l being Nat st
( S3[l] & ( for m being Nat st S3[m] holds
l <= m ) ) from NAT_1:sch_5(A14);
then consider l being Nat such that
A15: ( x < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . x & ( for m being Nat st x < m & (seq ^\ (1 + k1)) . m <= (seq ^\ (1 + k1)) . x holds
l <= m ) ) ;
take  l ; ::_thesis: ( l is Element of REAL & l is Element of NAT & S2[n,x,l] )
 l in NAT by ORDINAL1:def_12;
hence  ( l is Element of REAL & l is Element of NAT & S2[n,x,l] ) by A15; ::_thesis: verum
end;
consider f being Function of NAT,NAT such that
 f . 0 = 0 and
A16: for n being Element of NAT holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A13);
A17: dom f = NAT by FUNCT_2:def_1;
A18: rng f c= NAT by RELAT_1:def_19;
 rng f c= REAL ;
then reconsider f = f as Real_Sequence by A17, RELSET_1:4;
A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._n_is_Element_of_NAT
let n be Element of NAT ; ::_thesis: f . n is Element of NAT
 f . n in rng f by A17, FUNCT_1:def_3;
hence  f . n is Element of NAT by A18; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._n_<_f_._(n_+_1)
let n be Element of NAT ; ::_thesis: f . n < f . (n + 1)
 ( f . n is Element of NAT & f . (n + 1) is Element of NAT ) by A19;
hence  f . n < f . (n + 1) by A16; ::_thesis: verum
end;
then reconsider f = f as V39() sequence of NAT by SEQM_3:def_6;
consider Nseq being V39() sequence of NAT such that
A20: seq ^\ (1 + k1) = seq * Nseq by VALUED_0:def_17;
reconsider Nseq1 = Nseq * f as V39() sequence of NAT ;
take Nseq1 = Nseq1; ::_thesis: seq * Nseq1 is monotone
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_*_Nseq1)_._(n_+_1)_<=_(seq_*_Nseq1)_._n
let n be Element of NAT ; ::_thesis: (seq * Nseq1) . (n + 1) <= (seq * Nseq1) . n
 (seq ^\ (1 + k1)) . (f . (n + 1)) <= (seq ^\ (1 + k1)) . (f . n) by A16;
then  ((seq ^\ (1 + k1)) * f) . (n + 1) <= (seq ^\ (1 + k1)) . (f . n) by FUNCT_2:15;
then  ((seq * Nseq) * f) . (n + 1) <= ((seq ^\ (1 + k1)) * f) . n by A20, FUNCT_2:15;
then  (seq * Nseq1) . (n + 1) <= ((seq * Nseq) * f) . n by A20, RELAT_1:36;
hence  (seq * Nseq1) . (n + 1) <= (seq * Nseq1) . n by RELAT_1:36; ::_thesis: verum
end;
then  seq * Nseq1 is V42() by SEQM_3:def_9;
hence  seq * Nseq1 is monotone by SEQM_3:def_5; ::_thesis: verum
end;
now__::_thesis:_(_(_for_l_being_Element_of_NAT_ex_n_being_Element_of_NAT_st_
(_n_in_XN_&_not_n_<=_l_)_)_implies_ex_Nseq_being_V39()_sequence_of_NAT_st_seq_*_Nseq_is_monotone_)
defpred S2[ set , set , set ] means  for k, l being Element of NAT st k = $2 & l = $3 holds
( l in XN & k < l & ( for m being Element of NAT st m in XN & k < m holds
l <= m ) );
assume A21: for l being Element of NAT ex n being Element of NAT st
( n in XN & not n <= l ) ; ::_thesis: ex Nseq being V39() sequence of NAT st seq * Nseq is monotone
then consider n1 being Element of NAT  such that
A22: n1 in XN and
 not n1 <= 0 ;
reconsider 09 = n1 as Element of NAT ;
A23: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S2[n,x,y]
defpred S3[ Nat] means ( $1 in XN & x < $1 );
 ex n being Element of NAT st S3[n] by A21;
then A24: ex n being Nat st S3[n] ;
 ex l being Nat st
( S3[l] & ( for m being Nat st S3[m] holds
l <= m ) ) from NAT_1:sch_5(A24);
then consider l being Nat such that
A25: ( l in XN & x < l & ( for m being Nat st m in XN & x < m holds
l <= m ) ) ;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
take  l ; ::_thesis: S2[n,x,l]
thus  S2[n,x,l] by A25; ::_thesis: verum
end;
consider f being Function of NAT,NAT such that
A26: f . 0 = 09 and
A27: for n being Element of NAT holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A23);
A28: dom f = NAT by FUNCT_2:def_1;
A29: rng f c= NAT by RELAT_1:def_19;
 rng f c= REAL ;
then reconsider f = f as Real_Sequence by A28, RELSET_1:4;
A30: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_n_is_Element_of_NAT_&_f_._n_is_Element_of_NAT_&_f_._n_is_Element_of_NAT_)
let n be Element of NAT ; ::_thesis: ( n is Element of NAT & f . n is Element of NAT & f . n is Element of NAT )
thus  n is Element of NAT ; ::_thesis: ( f . n is Element of NAT & f . n is Element of NAT )
A31: f . n in rng f by A28, FUNCT_1:def_3;
hence  f . n is Element of NAT by A29; ::_thesis: f . n is Element of NAT
thus  f . n is Element of NAT by A29, A31; ::_thesis: verum
end;
A32: now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._n_<_f_._(n_+_1)
let n be Element of NAT ; ::_thesis: f . n < f . (n + 1)
 ( f . n is Element of NAT & f . (n + 1) is Element of NAT ) by A30;
hence  f . n < f . (n + 1) by A27; ::_thesis: verum
end;
A33: now__::_thesis:_for_n,_n_being_Element_of_NAT_holds_S3[n]
defpred S3[ Element of NAT ] means f . $1 in XN;
let n be Element of NAT ; ::_thesis: for n being Element of NAT holds S3[n]
A34: now__::_thesis:_for_k_being_Element_of_NAT_st_S3[k]_holds_
S3[k_+_1]
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume  S3[k] ; ::_thesis: S3[k + 1]
 ( f . k is Element of NAT & f . (k + 1) is Element of NAT ) by A30;
hence  S3[k + 1] by A27; ::_thesis: verum
end;
A35: S3[ 0 ] by A22, A26;
thus  for n being Element of NAT holds S3[n] from NAT_1:sch_1(A35, A34); ::_thesis: verum
end;
reconsider f = f as V39() sequence of NAT by A32, SEQM_3:def_6;
take Nseq = f; ::_thesis: seq * Nseq is monotone
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_*_Nseq)_._n_<_(seq_*_Nseq)_._(n_+_1)
let n be Element of NAT ; ::_thesis: (seq * Nseq) . n < (seq * Nseq) . (n + 1)
 ( Nseq . n in XN & Nseq . n < Nseq . (n + 1) ) by A33, A32;
then  seq . (Nseq . n) < seq . (Nseq . (n + 1)) by A1;
then  (seq * Nseq) . n < seq . (Nseq . (n + 1)) by FUNCT_2:15;
hence  (seq * Nseq) . n < (seq * Nseq) . (n + 1) by FUNCT_2:15; ::_thesis: verum
end;
then  seq * Nseq is V39() by SEQM_3:def_6;
hence  seq * Nseq is monotone by SEQM_3:def_5; ::_thesis: verum
end;
hence  ex Nseq being V39() sequence of NAT st seq * Nseq is monotone by A2; ::_thesis: verum
end;

theorem Th40: :: SEQ_4:40
for seq being Real_Sequence st seq is bounded holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is convergent ) )
assume A1: seq is bounded ; ::_thesis: ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )
consider Nseq being V39() sequence of NAT such that
A2: seq * Nseq is monotone by Th39;
take seq1 = seq * Nseq; ::_thesis: ( seq1 is subsequence of seq & seq1 is convergent )
thus  seq1 is subsequence of seq ; ::_thesis: seq1 is convergent
thus  seq1 is convergent by A1, A2, Th36, SEQM_3:29; ::_thesis: verum
end;

theorem :: SEQ_4:41
for seq being Real_Sequence holds
( seq is convergent iff for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s )
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent iff for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s )
thus  ( seq is convergent implies for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s ) ::_thesis: ( ( for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s ) implies seq is convergent )
proof
assume  seq is convergent ; ::_thesis: for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s
then consider g1 being real number  such that
A1: for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < s by SEQ_2:def_6;
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s )
assume  0 < s ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s
then consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < s / 2 by A1, XREAL_1:215;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - (seq . n)) < s )
assume  n <= m ; ::_thesis: abs ((seq . m) - (seq . n)) < s
then A3: abs ((seq . m) - g1) < s / 2 by A2;
A4: abs (((seq . m) - g1) + (g1 - (seq . n))) <= (abs ((seq . m) - g1)) + (abs (g1 - (seq . n))) by COMPLEX1:56;
 abs ((seq . n) - g1) < s / 2 by A2;
then  abs (- (g1 - (seq . n))) < s / 2 ;
then  abs (g1 - (seq . n)) < s / 2 by COMPLEX1:52;
then  (abs ((seq . m) - g1)) + (abs (g1 - (seq . n))) < (s / 2) + (s / 2) by A3, XREAL_1:8;
hence  abs ((seq . m) - (seq . n)) < s by A4, XXREAL_0:2; ::_thesis: verum
end;
assume A5: for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s ; ::_thesis: seq is convergent
then consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (seq . n1)) < 1 ;
consider r1 being real number  such that
A7: 0 < r1 and
A8: for m being Element of NAT st m <= n1 holds
abs (seq . m) < r1 by SEQ_2:4;
now__::_thesis:_ex_r_being_Element_of_REAL_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_holds_abs_(seq_._m)_<_r_)_)
take r = (r1 + (abs (seq . n1))) + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT holds abs (seq . m) < r ) )
 0 + 0 < r1 + (abs (seq . n1)) by A7, COMPLEX1:46, XREAL_1:8;
hence  0 < r ; ::_thesis: for m being Element of NAT holds abs (seq . m) < r
let m be Element of NAT ; ::_thesis: abs (seq . m) < r
A9: now__::_thesis:_(_n1_<=_m_implies_abs_(seq_._m)_<_r_)
assume  n1 <= m ; ::_thesis: abs (seq . m) < r
then A10: abs ((seq . m) - (seq . n1)) < 1 by A6;
 (abs (seq . m)) - (abs (seq . n1)) <= abs ((seq . m) - (seq . n1)) by COMPLEX1:59;
then  (abs (seq . m)) - (abs (seq . n1)) < 1 by A10, XXREAL_0:2;
then  ((abs (seq . m)) - (abs (seq . n1))) + (abs (seq . n1)) < 1 + (abs (seq . n1)) by XREAL_1:6;
then  0 + (abs (seq . m)) < r1 + ((abs (seq . n1)) + 1) by A7, XREAL_1:8;
hence  abs (seq . m) < r ; ::_thesis: verum
end;
now__::_thesis:_(_m_<=_n1_implies_abs_(seq_._m)_<_r_)
assume  m <= n1 ; ::_thesis: abs (seq . m) < r
then  abs (seq . m) < r1 by A8;
then  (abs (seq . m)) + 0 < r1 + (abs (seq . n1)) by COMPLEX1:46, XREAL_1:8;
hence  abs (seq . m) < r by XREAL_1:8; ::_thesis: verum
end;
hence  abs (seq . m) < r by A9; ::_thesis: verum
end;
then  seq is bounded by SEQ_2:3;
then consider seq1 being Real_Sequence such that
A11: seq1 is subsequence of seq and
A12: seq1 is convergent by Th40;
consider g1 being real number  such that
A13: for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g1) < s by A12, SEQ_2:def_6;
take  g1 ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs ((seq . b3) - g1) ) )
let s be real number ; ::_thesis: ( s <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not s <= abs ((seq . b2) - g1) ) )
assume A14: 0 < s ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not s <= abs ((seq . b2) - g1) )
then consider n1 being Element of NAT  such that
A15: for m being Element of NAT st n1 <= m holds
abs ((seq1 . m) - g1) < s / 3 by A13, XREAL_1:222;
consider n2 being Element of NAT  such that
A16: for m being Element of NAT st n2 <= m holds
abs ((seq . m) - (seq . n2)) < s / 3 by A5, A14, XREAL_1:222;
take n = n1 + n2; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not s <= abs ((seq . b1) - g1) )
let m be Element of NAT ; ::_thesis: ( not n <= m or not s <= abs ((seq . m) - g1) )
assume A17: n <= m ; ::_thesis: not s <= abs ((seq . m) - g1)
consider Nseq being V39() sequence of NAT such that
A18: seq1 = seq * Nseq by A11, VALUED_0:def_17;
 n1 <= n by NAT_1:12;
then  n1 <= m by A17, XXREAL_0:2;
then  abs (((seq * Nseq) . m) - g1) < s / 3 by A18, A15;
then A19: abs ((seq . (Nseq . m)) - g1) < s / 3 by FUNCT_2:15;
 n2 <= n by NAT_1:12;
then A20: n2 <= m by A17, XXREAL_0:2;
 m <= Nseq . m by SEQM_3:14;
then  n2 <= Nseq . m by A20, XXREAL_0:2;
then  abs ((seq . (Nseq . m)) - (seq . n2)) < s / 3 by A16;
then  abs (- ((seq . n2) - (seq . (Nseq . m)))) < s / 3 ;
then A21: abs ((seq . n2) - (seq . (Nseq . m))) < s / 3 by COMPLEX1:52;
 abs ((seq . m) - (seq . n2)) < s / 3 by A16, A20;
then A22: (abs ((seq . m) - (seq . n2))) + (abs ((seq . n2) - (seq . (Nseq . m)))) < (s / 3) + (s / 3) by A21, XREAL_1:8;
 abs (((seq . m) - (seq . n2)) + ((seq . n2) - (seq . (Nseq . m)))) <= (abs ((seq . m) - (seq . n2))) + (abs ((seq . n2) - (seq . (Nseq . m)))) by COMPLEX1:56;
then  abs ((seq . m) - (seq . (Nseq . m))) < (s / 3) + (s / 3) by A22, XXREAL_0:2;
then A23: (abs ((seq . m) - (seq . (Nseq . m)))) + (abs ((seq . (Nseq . m)) - g1)) < ((s / 3) + (s / 3)) + (s / 3) by A19, XREAL_1:8;
 abs (((seq . m) - (seq . (Nseq . m))) + ((seq . (Nseq . m)) - g1)) <= (abs ((seq . m) - (seq . (Nseq . m)))) + (abs ((seq . (Nseq . m)) - g1)) by COMPLEX1:56;
hence  not s <= abs ((seq . m) - g1) by A23, XXREAL_0:2; ::_thesis: verum
end;

theorem :: SEQ_4:42
for seq, seq1 being Real_Sequence st seq is constant & seq1 is convergent holds
( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is constant & seq1 is convergent implies ( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) ) )
assume that
A1: seq is constant and
A2: seq1 is convergent ; ::_thesis: ( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
thus  lim (seq + seq1) = (lim seq) + (lim seq1) by A1, A2, SEQ_2:6
.= (seq . 0) + (lim seq1) by A1, Th25 ; ::_thesis: ( lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
thus  lim (seq - seq1) = (lim seq) - (lim seq1) by A1, A2, SEQ_2:12
.= (seq . 0) - (lim seq1) by A1, Th25 ; ::_thesis: ( lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
thus  lim (seq1 - seq) = (lim seq1) - (lim seq) by A1, A2, SEQ_2:12
.= (lim seq1) - (seq . 0) by A1, Th25 ; ::_thesis: lim (seq (#) seq1) = (seq . 0) * (lim seq1)
thus  lim (seq (#) seq1) = (lim seq) * (lim seq1) by A1, A2, SEQ_2:15
.= (seq . 0) * (lim seq1) by A1, Th25 ; ::_thesis: verum
end;

begin

theorem Th43: :: SEQ_4:43
for X being non empty real-membered set
for t being real number st ( for s being real number st s in X holds
s >= t ) holds
lower_bound X >= t
proof
let X be non empty real-membered set ; ::_thesis: for t being real number st ( for s being real number st s in X holds
s >= t ) holds
lower_bound X >= t
set r = lower_bound X;
let t be real number ; ::_thesis: ( ( for s being real number st s in X holds
s >= t ) implies lower_bound X >= t )
assume A1: for s being real number st s in X holds
s >= t ; ::_thesis: lower_bound X >= t
set s = t - (lower_bound X);
assume  lower_bound X < t ; ::_thesis: contradiction
then A2: t - (lower_bound X) > 0 by XREAL_1:50;
 X is bounded_below
proof
take  t ; :: according to XXREAL_2:def_9 ::_thesis: t is LowerBound of X
let s be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not s in X or t <= s )
thus  ( not s in X or t <= s ) by A1; ::_thesis: verum
end;
then  ex t9 being real number st
( t9 in X & t9 < (lower_bound X) + (t - (lower_bound X)) ) by A2, Def2;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th44: :: SEQ_4:44
for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X by Lm1;

theorem Th45: :: SEQ_4:45
for X being non empty real-membered set
for r, t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t
proof
let X be non empty real-membered set ; ::_thesis: for r, t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t
let r be real number ; ::_thesis: for t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t
set r = upper_bound X;
let t be real number ; ::_thesis: ( ( for s being real number st s in X holds
s <= t ) implies upper_bound X <= t )
assume A1: for s being real number st s in X holds
s <= t ; ::_thesis: upper_bound X <= t
set s = (upper_bound X) - t;
assume  upper_bound X > t ; ::_thesis: contradiction
then A2: (upper_bound X) - t > 0 by XREAL_1:50;
 X is bounded_above
proof
take  t ; :: according to XXREAL_2:def_10 ::_thesis: t is UpperBound of X
let s be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not s in X or s <= t )
thus  ( not s in X or s <= t ) by A1; ::_thesis: verum
end;
then  ex t9 being real number st
( t9 in X & (upper_bound X) - ((upper_bound X) - t) < t9 ) by A2, Def1;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th46: :: SEQ_4:46
for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X by Lm2;

theorem :: SEQ_4:47
for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_below holds
lower_bound Y <= lower_bound X
proof
let X be non empty real-membered set ; ::_thesis: for Y being real-membered set st X c= Y & Y is bounded_below holds
lower_bound Y <= lower_bound X
let Y be real-membered set ; ::_thesis: ( X c= Y & Y is bounded_below implies lower_bound Y <= lower_bound X )
assume  ( X c= Y & Y is bounded_below ) ; ::_thesis: lower_bound Y <= lower_bound X
then  for t being real number st t in X holds
t >= lower_bound Y by Def2;
hence  lower_bound Y <= lower_bound X by Th43; ::_thesis: verum
end;

theorem :: SEQ_4:48
for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_above holds
upper_bound X <= upper_bound Y
proof
let X be non empty real-membered set ; ::_thesis: for Y being real-membered set st X c= Y & Y is bounded_above holds
upper_bound X <= upper_bound Y
let Y be real-membered set ; ::_thesis: ( X c= Y & Y is bounded_above implies upper_bound X <= upper_bound Y )
assume  ( X c= Y & Y is bounded_above ) ; ::_thesis: upper_bound X <= upper_bound Y
then  for t being real number st t in X holds
t <= upper_bound Y by Def1;
hence  upper_bound X <= upper_bound Y by Th45; ::_thesis: verum
end;

definition
let A be non empty natural-membered set ;
:: original: inf
redefine func min A ->  Element of NAT ;
coherence
 inf A is Element of NAT by ORDINAL1:def_12;
end;

begin


theorem :: SEQ_4:49
0c is_a_unity_wrt addcomplex by BINOP_2:1, SETWISEO:14;

theorem Th50: :: SEQ_4:50
compcomplex is_an_inverseOp_wrt addcomplex
proof
let c be Element of COMPLEX ; :: according to FINSEQOP:def_1 ::_thesis: ( addcomplex . (c,(compcomplex . c)) = the_unity_wrt addcomplex & addcomplex . ((compcomplex . c),c) = the_unity_wrt addcomplex )
thus addcomplex . (c,(compcomplex . c)) = c + (compcomplex . c) by BINOP_2:def_3
.= c + (- c) by BINOP_2:def_1
.= the_unity_wrt addcomplex by BINOP_2:1 ; ::_thesis: addcomplex . ((compcomplex . c),c) = the_unity_wrt addcomplex
thus addcomplex . ((compcomplex . c),c) = (compcomplex . c) + c by BINOP_2:def_3
.= (- c) + c by BINOP_2:def_1
.= the_unity_wrt addcomplex by BINOP_2:1 ; ::_thesis: verum
end;

theorem Th51: :: SEQ_4:51
addcomplex is having_an_inverseOp by Th50, FINSEQOP:def_2;

theorem Th52: :: SEQ_4:52
the_inverseOp_wrt addcomplex = compcomplex by Th50, Th51, FINSEQOP:def_3;

definition
redefine func diffcomplex  equals :: SEQ_4:def 3
addcomplex * ((id COMPLEX),compcomplex);
compatibility
 for b1 being Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:] holds
( b1 = diffcomplex iff b1 = addcomplex * ((id COMPLEX),compcomplex) )
proof
let b be BinOp of COMPLEX; ::_thesis: ( b = diffcomplex iff b = addcomplex * ((id COMPLEX),compcomplex) )
now__::_thesis:_for_c1,_c2_being_Element_of_COMPLEX_holds_diffcomplex_._(c1,c2)_=_(addcomplex_*_((id_COMPLEX),compcomplex))_._(c1,c2)
let c1, c2 be Element of COMPLEX ; ::_thesis: diffcomplex . (c1,c2) = (addcomplex * ((id COMPLEX),compcomplex)) . (c1,c2)
thus diffcomplex . (c1,c2) = c1 - c2 by BINOP_2:def_4
.= c1 + (- c2)
.= addcomplex . (c1,(- c2)) by BINOP_2:def_3
.= addcomplex . (c1,(compcomplex . c2)) by BINOP_2:def_1
.= (addcomplex * ((id COMPLEX),compcomplex)) . (c1,c2) by FINSEQOP:82 ; ::_thesis: verum
end;
hence  ( b = diffcomplex iff b = addcomplex * ((id COMPLEX),compcomplex) ) by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines diffcomplex SEQ_4:def_3_:_
 diffcomplex = addcomplex * ((id COMPLEX),compcomplex);

theorem :: SEQ_4:53
1r is_a_unity_wrt multcomplex by BINOP_2:6, SETWISEO:14;

theorem Th54: :: SEQ_4:54
multcomplex is_distributive_wrt addcomplex
proof
now__::_thesis:_for_c1,_c2,_c3_being_Element_of_COMPLEX_holds_
(_multcomplex_._(c1,(addcomplex_._(c2,c3)))_=_addcomplex_._((multcomplex_._(c1,c2)),(multcomplex_._(c1,c3)))_&_multcomplex_._((addcomplex_._(c1,c2)),c3)_=_addcomplex_._((multcomplex_._(c1,c3)),(multcomplex_._(c2,c3)))_)
let c1, c2, c3 be Element of COMPLEX ; ::_thesis: ( multcomplex . (c1,(addcomplex . (c2,c3))) = addcomplex . ((multcomplex . (c1,c2)),(multcomplex . (c1,c3))) & multcomplex . ((addcomplex . (c1,c2)),c3) = addcomplex . ((multcomplex . (c1,c3)),(multcomplex . (c2,c3))) )
thus multcomplex . (c1,(addcomplex . (c2,c3))) = multcomplex . (c1,(c2 + c3)) by BINOP_2:def_3
.= c1 * (c2 + c3) by BINOP_2:def_5
.= (c1 * c2) + (c1 * c3)
.= addcomplex . ((c1 * c2),(c1 * c3)) by BINOP_2:def_3
.= addcomplex . ((multcomplex . (c1,c2)),(c1 * c3)) by BINOP_2:def_5
.= addcomplex . ((multcomplex . (c1,c2)),(multcomplex . (c1,c3))) by BINOP_2:def_5 ; ::_thesis: multcomplex . ((addcomplex . (c1,c2)),c3) = addcomplex . ((multcomplex . (c1,c3)),(multcomplex . (c2,c3)))
thus multcomplex . ((addcomplex . (c1,c2)),c3) = multcomplex . ((c1 + c2),c3) by BINOP_2:def_3
.= (c1 + c2) * c3 by BINOP_2:def_5
.= (c1 * c3) + (c2 * c3)
.= addcomplex . ((c1 * c3),(c2 * c3)) by BINOP_2:def_3
.= addcomplex . ((multcomplex . (c1,c3)),(c2 * c3)) by BINOP_2:def_5
.= addcomplex . ((multcomplex . (c1,c3)),(multcomplex . (c2,c3))) by BINOP_2:def_5 ; ::_thesis: verum
end;
hence  multcomplex is_distributive_wrt addcomplex by BINOP_1:11; ::_thesis: verum
end;

definition
let c be complex number ;
funcc multcomplex  ->  UnOp of COMPLEX equals :: SEQ_4:def 4
multcomplex [;] (c,(id COMPLEX));
coherence
 multcomplex [;] (c,(id COMPLEX)) is UnOp of COMPLEX
proof
reconsider c9 = c as Element of COMPLEX by XCMPLX_0:def_2;
 multcomplex [;] (c9,(id COMPLEX)) is UnOp of COMPLEX ;
hence  multcomplex [;] (c,(id COMPLEX)) is UnOp of COMPLEX ; ::_thesis: verum
end;
end;

:: deftheorem  defines multcomplex SEQ_4:def_4_:_
 for c being complex number holds c multcomplex = multcomplex [;] (c,(id COMPLEX));

Lm3:  for c, c9 being Element of COMPLEX holds (multcomplex [;] (c,(id COMPLEX))) . c9 = c * c9
proof
let c, c9 be Element of COMPLEX ; ::_thesis: (multcomplex [;] (c,(id COMPLEX))) . c9 = c * c9
thus (multcomplex [;] (c,(id COMPLEX))) . c9 = multcomplex . (c,((id COMPLEX) . c9)) by FUNCOP_1:53
.= multcomplex . (c,c9) by FUNCT_1:18
.= c * c9 by BINOP_2:def_5 ; ::_thesis: verum
end;

theorem :: SEQ_4:55
for c, c9 being Element of COMPLEX holds (c multcomplex) . c9 = c * c9 by Lm3;

theorem :: SEQ_4:56
for c being Element of COMPLEX holds c multcomplex is_distributive_wrt addcomplex by Th54, FINSEQOP:54;

definition
func abscomplex  ->  Function of COMPLEX,REAL means :Def5: :: SEQ_4:def 5
 for c being Element of COMPLEX holds it . c = |.c.|;
existence
 ex b1 being Function of COMPLEX,REAL st
for c being Element of COMPLEX holds b1 . c = |.c.| from FUNCT_2:sch_4();
uniqueness
 for b1, b2 being Function of COMPLEX,REAL st ( for c being Element of COMPLEX holds b1 . c = |.c.| ) & ( for c being Element of COMPLEX holds b2 . c = |.c.| ) holds
b1 = b2 from BINOP_2:sch_1();
end;

:: deftheorem Def5 defines abscomplex SEQ_4:def_5_:_
 for b1 being Function of COMPLEX,REAL holds
( b1 = abscomplex iff for c being Element of COMPLEX holds b1 . c = |.c.| );


definition
let z1, z2 be FinSequence of COMPLEX ;
:: original: +
redefine funcz1 + z2 ->  FinSequence of COMPLEX  equals :: SEQ_4:def 6
addcomplex .: (z1,z2);
coherence
 z1 + z2 is FinSequence of COMPLEX
proof
thus  rng (z1 + z2) c= COMPLEX ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = z1 + z2 iff b1 = addcomplex .: (z1,z2) )
proof
set g = addcomplex .: (z1,z2);
 dom addcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def_1;
then  [:(rng z1),(rng z2):] c= dom addcomplex by ZFMISC_1:96;
then A1: ( dom (z1 + z2) = (dom z1) /\ (dom z2) & dom (addcomplex .: (z1,z2)) = (dom z1) /\ (dom z2) ) by FUNCOP_1:69, VALUED_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(z1_+_z2)_holds_
(z1_+_z2)_._x_=_(addcomplex_.:_(z1,z2))_._x
let x be set ; ::_thesis: ( x in dom (z1 + z2) implies (z1 + z2) . x = (addcomplex .: (z1,z2)) . x )
assume A2: x in dom (z1 + z2) ; ::_thesis: (z1 + z2) . x = (addcomplex .: (z1,z2)) . x
hence (z1 + z2) . x = (z1 . x) + (z2 . x) by VALUED_1:def_1
.= addcomplex . ((z1 . x),(z2 . x)) by BINOP_2:def_3
.= (addcomplex .: (z1,z2)) . x by A1, A2, FUNCOP_1:22 ;
::_thesis: verum
end;
hence  for b1 being FinSequence of COMPLEX holds
( b1 = z1 + z2 iff b1 = addcomplex .: (z1,z2) ) by A1, FUNCT_1:2; ::_thesis: verum
end;
:: original: -
redefine funcz1 - z2 ->  FinSequence of COMPLEX  equals :: SEQ_4:def 7
diffcomplex .: (z1,z2);
coherence
 z1 - z2 is FinSequence of COMPLEX
proof
thus  rng (z1 - z2) c= COMPLEX ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = z1 - z2 iff b1 = diffcomplex .: (z1,z2) )
proof
set g = diffcomplex .: (z1,z2);
 dom diffcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def_1;
then  [:(rng z1),(rng z2):] c= dom diffcomplex by ZFMISC_1:96;
then A3: dom (diffcomplex .: (z1,z2)) = (dom z1) /\ (dom z2) by FUNCOP_1:69;
A4: dom (z1 - z2) = (dom z1) /\ (dom z2) by VALUED_1:12;
now__::_thesis:_for_x_being_set_st_x_in_dom_(z1_-_z2)_holds_
(z1_-_z2)_._x_=_(diffcomplex_.:_(z1,z2))_._x
let x be set ; ::_thesis: ( x in dom (z1 - z2) implies (z1 - z2) . x = (diffcomplex .: (z1,z2)) . x )
assume A5: x in dom (z1 - z2) ; ::_thesis: (z1 - z2) . x = (diffcomplex .: (z1,z2)) . x
hence (z1 - z2) . x = (z1 . x) - (z2 . x) by VALUED_1:13
.= diffcomplex . ((z1 . x),(z2 . x)) by BINOP_2:def_4
.= (diffcomplex .: (z1,z2)) . x by A4, A3, A5, FUNCOP_1:22 ;
::_thesis: verum
end;
hence  for b1 being FinSequence of COMPLEX holds
( b1 = z1 - z2 iff b1 = diffcomplex .: (z1,z2) ) by A3, FUNCT_1:2, VALUED_1:12; ::_thesis: verum
end;
end;

:: deftheorem  defines + SEQ_4:def_6_:_
 for z1, z2 being FinSequence of COMPLEX holds z1 + z2 = addcomplex .: (z1,z2);

:: deftheorem  defines - SEQ_4:def_7_:_
 for z1, z2 being FinSequence of COMPLEX holds z1 - z2 = diffcomplex .: (z1,z2);

definition
let z be FinSequence of COMPLEX ;
:: original: -
redefine func - z ->  FinSequence of COMPLEX  equals :: SEQ_4:def 8
compcomplex * z;
coherence
 - z is FinSequence of COMPLEX
proof
thus  rng (- z) c= COMPLEX ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = - z iff b1 = compcomplex * z )
proof
set g = compcomplex * z;
 dom compcomplex = COMPLEX by FUNCT_2:def_1;
then  rng z c= dom compcomplex ;
then A1: dom (compcomplex * z) = dom z by RELAT_1:27;
A2: dom (- z) = dom z by VALUED_1:8;
now__::_thesis:_for_x_being_set_st_x_in_dom_(-_z)_holds_
(-_z)_._x_=_(compcomplex_*_z)_._x
let x be set ; ::_thesis: ( x in dom (- z) implies (- z) . x = (compcomplex * z) . x )
assume A3: x in dom (- z) ; ::_thesis: (- z) . x = (compcomplex * z) . x
thus (- z) . x = - (z . x) by VALUED_1:8
.= compcomplex . (z . x) by BINOP_2:def_1
.= (compcomplex * z) . x by A2, A1, A3, FUNCT_1:12 ; ::_thesis: verum
end;
hence  for b1 being FinSequence of COMPLEX holds
( b1 = - z iff b1 = compcomplex * z ) by A1, FUNCT_1:2, VALUED_1:8; ::_thesis: verum
end;
end;

:: deftheorem  defines - SEQ_4:def_8_:_
 for z being FinSequence of COMPLEX holds - z = compcomplex * z;

notation
let z be FinSequence of COMPLEX ;
let c be complex number ;
synonym c * z for c (#) z;
end;

definition
let z be FinSequence of COMPLEX ;
let c be complex number ;
:: original: *
redefine funcc * z ->  FinSequence of COMPLEX  equals :: SEQ_4:def 9
(c multcomplex) * z;
coherence
 c * z is FinSequence of COMPLEX
proof
thus  rng (c (#) z) c= COMPLEX ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = c * z iff b1 = (c multcomplex) * z )
proof
set g = (c multcomplex) * z;
 dom (c multcomplex) = COMPLEX by FUNCT_2:def_1;
then  rng z c= dom (c multcomplex) ;
then A1: ( dom (c (#) z) = dom z & dom ((c multcomplex) * z) = dom z ) by RELAT_1:27, VALUED_1:def_5;
now__::_thesis:_for_x_being_set_st_x_in_dom_(c_(#)_z)_holds_
(c_(#)_z)_._x_=_((c_multcomplex)_*_z)_._x
let x be set ; ::_thesis: ( x in dom (c (#) z) implies (c (#) z) . x = ((c multcomplex) * z) . x )
assume A2: x in dom (c (#) z) ; ::_thesis: (c (#) z) . x = ((c multcomplex) * z) . x
A3: ( c is Element of COMPLEX & z . x is Element of COMPLEX ) by XCMPLX_0:def_2;
thus (c (#) z) . x = c * (z . x) by VALUED_1:6
.= (c multcomplex) . (z . x) by A3, Lm3
.= ((c multcomplex) * z) . x by A1, A2, FUNCT_1:12 ; ::_thesis: verum
end;
hence  for b1 being FinSequence of COMPLEX holds
( b1 = c * z iff b1 = (c multcomplex) * z ) by A1, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines * SEQ_4:def_9_:_
 for z being FinSequence of COMPLEX
for c being complex number holds c * z = (c multcomplex) * z;

definition
let z be FinSequence of COMPLEX ;
:: original: |.
redefine func abs z ->  FinSequence of REAL  equals :: SEQ_4:def 10
abscomplex * z;
coherence
 |.z.| is FinSequence of REAL
proof
thus  rng (abs z) c= REAL ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
compatibility
 for b1 being FinSequence of REAL holds
( b1 = |.z.| iff b1 = abscomplex * z )
proof
set g = abscomplex * z;
 dom abscomplex = COMPLEX by FUNCT_2:def_1;
then  rng z c= dom abscomplex ;
then A1: ( dom (abs z) = dom z & dom (abscomplex * z) = dom z ) by RELAT_1:27, VALUED_1:def_11;
now__::_thesis:_for_x_being_set_st_x_in_dom_(abs_z)_holds_
(abs_z)_._x_=_(abscomplex_*_z)_._x
let x be set ; ::_thesis: ( x in dom (abs z) implies (abs z) . x = (abscomplex * z) . x )
assume A2: x in dom (abs z) ; ::_thesis: (abs z) . x = (abscomplex * z) . x
A3: z . x is Element of COMPLEX by XCMPLX_0:def_2;
thus (abs z) . x = abs (z . x) by VALUED_1:18
.= abscomplex . (z . x) by A3, Def5
.= (abscomplex * z) . x by A1, A2, FUNCT_1:12 ; ::_thesis: verum
end;
hence  for b1 being FinSequence of REAL holds
( b1 = |.z.| iff b1 = abscomplex * z ) by A1, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines abs SEQ_4:def_10_:_
 for z being FinSequence of COMPLEX holds abs z = abscomplex * z;

definition
let n be Element of NAT ;
func COMPLEX n ->  FinSequenceSet of COMPLEX  equals :: SEQ_4:def 11
n -tuples_on COMPLEX;
correctness
coherence
n -tuples_on COMPLEX is FinSequenceSet of COMPLEX ;
;
end;

:: deftheorem  defines COMPLEX SEQ_4:def_11_:_
 for n being Element of NAT holds COMPLEX n = n -tuples_on COMPLEX;

registration
let n be Element of NAT ;
cluster COMPLEX n ->  non empty ;
coherence
 not COMPLEX n is empty ;
end;

       Lm4:  for n being Element of NAT
for z being Element of COMPLEX n holds dom z = Seg n
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n holds dom z = Seg n
let z be Element of COMPLEX n; ::_thesis: dom z = Seg n
 len z = n by CARD_1:def_7;
hence  dom z = Seg n by FINSEQ_1:def_3; ::_thesis: verum
end;

theorem Th57: :: SEQ_4:57
for k, n being Element of NAT
for z being Element of COMPLEX n st k in Seg n holds
z . k in COMPLEX
proof
let k, n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n st k in Seg n holds
z . k in COMPLEX
let z be Element of COMPLEX n; ::_thesis: ( k in Seg n implies z . k in COMPLEX )
 len z = n by CARD_1:def_7;
then  Seg n = dom z by FINSEQ_1:def_3;
hence  ( k in Seg n implies z . k in COMPLEX ) by FINSEQ_2:11; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let z1, z2 be Element of COMPLEX n;
:: original: +
redefine funcz1 + z2 ->  Element of COMPLEX n;
coherence
 z1 + z2 is Element of COMPLEX n by FINSEQ_2:120;
end;

theorem Th58: :: SEQ_4:58
for k, n being Element of NAT
for c1, c2 being Element of COMPLEX
for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds
(z1 + z2) . k = c1 + c2
proof
let k, n be Element of NAT ; ::_thesis: for c1, c2 being Element of COMPLEX
for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds
(z1 + z2) . k = c1 + c2
let c1, c2 be Element of COMPLEX ; ::_thesis: for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds
(z1 + z2) . k = c1 + c2
let z1, z2 be Element of COMPLEX n; ::_thesis: ( k in Seg n & c1 = z1 . k & c2 = z2 . k implies (z1 + z2) . k = c1 + c2 )
assume that
A1: k in Seg n and
A2: ( c1 = z1 . k & c2 = z2 . k ) ; ::_thesis: (z1 + z2) . k = c1 + c2
 k in dom (z1 + z2) by A1, Lm4;
hence (z1 + z2) . k = addcomplex . (c1,c2) by A2, FUNCOP_1:22
.= c1 + c2 by BINOP_2:def_3 ;
::_thesis: verum
end;

definition
let n be Element of NAT ;
func 0c n ->  FinSequence of COMPLEX  equals :: SEQ_4:def 12
n |-> 0c;
correctness
coherence
n |-> 0c is FinSequence of COMPLEX ;
;
end;

:: deftheorem  defines 0c SEQ_4:def_12_:_
 for n being Element of NAT holds 0c n = n |-> 0c;

definition
let n be Element of NAT ;
:: original: 0c
redefine func 0c n ->  Element of COMPLEX n;
coherence
 0c n is Element of COMPLEX n ;
end;

theorem :: SEQ_4:59
for n being Element of NAT
for z being Element of COMPLEX n holds
( z + (0c n) = z & z = (0c n) + z ) by BINOP_2:1, FINSEQOP:56;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
:: original: -
redefine func - z ->  Element of COMPLEX n;
coherence
 - z is Element of COMPLEX n by FINSEQ_2:113;
end;

theorem Th60: :: SEQ_4:60
for k, n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(- z) . k = - c
proof
let k, n be Element of NAT ; ::_thesis: for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(- z) . k = - c
let c be Element of COMPLEX ; ::_thesis: for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(- z) . k = - c
let z be Element of COMPLEX n; ::_thesis: ( k in Seg n & c = z . k implies (- z) . k = - c )
assume that
A1: k in Seg n and
A2: c = z . k ; ::_thesis: (- z) . k = - c
 k in dom (- z) by A1, Lm4;
hence (- z) . k = compcomplex . c by A2, FUNCT_1:12
.= - c by BINOP_2:def_1 ;
::_thesis: verum
end;

Lm5:  for n being Element of NAT holds - (0c n) = 0c n
proof
let n be Element of NAT ; ::_thesis: - (0c n) = 0c n
thus  - (0c n) = n |-> (compcomplex . 0c) by FINSEQOP:16
.= n |-> (- 0c) by BINOP_2:def_1
.= 0c n ; ::_thesis: verum
end;

theorem :: SEQ_4:61
for n being Element of NAT
for z being Element of COMPLEX n holds
( z + (- z) = 0c n & (- z) + z = 0c n ) by Th51, Th52, BINOP_2:1, FINSEQOP:73;

theorem :: SEQ_4:62
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 + z2 = 0c n holds
( z1 = - z2 & z2 = - z1 ) by Th51, Th52, BINOP_2:1, FINSEQOP:74;

theorem :: SEQ_4:63
canceled;

theorem :: SEQ_4:64
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st - z1 = - z2 holds
z1 = z2
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n st - z1 = - z2 holds
z1 = z2
let z1, z2 be Element of COMPLEX n; ::_thesis: ( - z1 = - z2 implies z1 = z2 )
assume  - z1 = - z2 ; ::_thesis: z1 = z2
hence z1 = - (- z2)
.= z2 ;
::_thesis: verum
end;

Lm6:  for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
proof
let n be Element of NAT ; ::_thesis: for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
let z1, z, z2 be Element of COMPLEX n; ::_thesis: ( z1 + z = z2 + z implies z1 = z2 )
assume  z1 + z = z2 + z ; ::_thesis: z1 = z2
then  z1 + (z + (- z)) = (z2 + z) + (- z) by FINSEQOP:28;
then A1: z1 + (z + (- z)) = z2 + (z + (- z)) by FINSEQOP:28;
 z + (- z) = 0c n by Th51, Th52, BINOP_2:1, FINSEQOP:73;
then  z1 = z2 + (0c n) by A1, BINOP_2:1, FINSEQOP:56;
hence  z1 = z2 by BINOP_2:1, FINSEQOP:56; ::_thesis: verum
end;

theorem :: SEQ_4:65
for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st ( z1 + z = z2 + z or z1 + z = z + z2 ) holds
z1 = z2 by Lm6;

theorem Th66: :: SEQ_4:66
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2)
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2)
let z1, z2 be Element of COMPLEX n; ::_thesis: - (z1 + z2) = (- z1) + (- z2)
(z1 + z2) + ((- z1) + (- z2)) = ((z2 + z1) + (- z1)) + (- z2) by FINSEQOP:28
.= (z2 + (z1 + (- z1))) + (- z2) by FINSEQOP:28
.= (z2 + (0c n)) + (- z2) by Th51, Th52, BINOP_2:1, FINSEQOP:73
.= z2 + (- z2) by BINOP_2:1, FINSEQOP:56
.= 0c n by Th51, Th52, BINOP_2:1, FINSEQOP:73 ;
hence  - (z1 + z2) = (- z1) + (- z2) by Th51, Th52, BINOP_2:1, FINSEQOP:74; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let z1, z2 be Element of COMPLEX n;
:: original: -
redefine funcz1 - z2 ->  Element of COMPLEX n;
coherence
 z1 - z2 is Element of COMPLEX n by FINSEQ_2:120;
end;

theorem :: SEQ_4:67
for k, n being Element of NAT
for z1, z2 being Element of COMPLEX n st k in Seg n holds
(z1 - z2) . k = (z1 . k) - (z2 . k)
proof
let k, n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n st k in Seg n holds
(z1 - z2) . k = (z1 . k) - (z2 . k)
let z1, z2 be Element of COMPLEX n; ::_thesis: ( k in Seg n implies (z1 - z2) . k = (z1 . k) - (z2 . k) )
assume A1: k in Seg n ; ::_thesis: (z1 - z2) . k = (z1 . k) - (z2 . k)
set c1 = z1 . k;
set c2 = z2 . k;
 k in dom (z1 - z2) by A1, Lm4;
hence (z1 - z2) . k = diffcomplex . ((z1 . k),(z2 . k)) by FUNCOP_1:22
.= (z1 . k) - (z2 . k) by BINOP_2:def_4 ;
::_thesis: verum
end;

theorem :: SEQ_4:68
for n being Element of NAT
for z being Element of COMPLEX n holds z - (0c n) = z
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n holds z - (0c n) = z
let z be Element of COMPLEX n; ::_thesis: z - (0c n) = z
thus z - (0c n) = z + (0c n) by Lm5
.= z by BINOP_2:1, FINSEQOP:56 ; ::_thesis: verum
end;

theorem :: SEQ_4:69
for n being Element of NAT
for z being Element of COMPLEX n holds (0c n) - z = - z
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n holds (0c n) - z = - z
let z be Element of COMPLEX n; ::_thesis: (0c n) - z = - z
thus (0c n) - z = (0c n) + (- z)
.= - z by BINOP_2:1, FINSEQOP:56 ; ::_thesis: verum
end;

theorem :: SEQ_4:70
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds z1 - (- z2) = z1 + z2 ;

theorem Th71: :: SEQ_4:71
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = z2 - z1
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = z2 - z1
let z1, z2 be Element of COMPLEX n; ::_thesis: - (z1 - z2) = z2 - z1
thus  - (z1 - z2) = (- z1) + (- (- z2)) by Th66
.= z2 - z1 ; ::_thesis: verum
end;

theorem Th72: :: SEQ_4:72
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = (- z1) + z2
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = (- z1) + z2
let z1, z2 be Element of COMPLEX n; ::_thesis: - (z1 - z2) = (- z1) + z2
thus  - (z1 - z2) = (- z1) + (- (- z2)) by Th66
.= (- z1) + z2 ; ::_thesis: verum
end;

theorem Th73: :: SEQ_4:73
for n being Element of NAT
for z being Element of COMPLEX n holds z - z = 0c n
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n holds z - z = 0c n
let z be Element of COMPLEX n; ::_thesis: z - z = 0c n
thus z - z = z + (- z)
.= 0c n by Th51, Th52, BINOP_2:1, FINSEQOP:73 ; ::_thesis: verum
end;

theorem Th74: :: SEQ_4:74
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 - z2 = 0c n holds
z1 = z2
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n st z1 - z2 = 0c n holds
z1 = z2
let z1, z2 be Element of COMPLEX n; ::_thesis: ( z1 - z2 = 0c n implies z1 = z2 )
assume  z1 - z2 = 0c n ; ::_thesis: z1 = z2
then  z1 + (- z2) = 0c n ;
then  z1 = - (- z2) by Th51, Th52, BINOP_2:1, FINSEQOP:74;
hence  z1 = z2 ; ::_thesis: verum
end;

theorem Th75: :: SEQ_4:75
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) - z3 = z1 - (z2 + z3)
proof
let n be Element of NAT ; ::_thesis: for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) - z3 = z1 - (z2 + z3)
let z1, z2, z3 be Element of COMPLEX n; ::_thesis: (z1 - z2) - z3 = z1 - (z2 + z3)
thus (z1 - z2) - z3 = (z1 + (- z2)) + (- z3)
.= z1 + ((- z2) + (- z3)) by FINSEQOP:28
.= z1 - (z2 + z3) by Th66 ; ::_thesis: verum
end;

theorem Th76: :: SEQ_4:76
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 - z3) = (z1 + z2) - z3
proof
let n be Element of NAT ; ::_thesis: for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 - z3) = (z1 + z2) - z3
let z1, z2, z3 be Element of COMPLEX n; ::_thesis: z1 + (z2 - z3) = (z1 + z2) - z3
thus z1 + (z2 - z3) = z1 + (z2 + (- z3))
.= (z1 + z2) + (- z3) by FINSEQOP:28
.= (z1 + z2) - z3 ; ::_thesis: verum
end;

theorem :: SEQ_4:77
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds z1 - (z2 - z3) = (z1 - z2) + z3
proof
let n be Element of NAT ; ::_thesis: for z1, z2, z3 being Element of COMPLEX n holds z1 - (z2 - z3) = (z1 - z2) + z3
let z1, z2, z3 be Element of COMPLEX n; ::_thesis: z1 - (z2 - z3) = (z1 - z2) + z3
thus z1 - (z2 - z3) = z1 + ((- z2) + z3) by Th72
.= (z1 + (- z2)) + z3 by FINSEQOP:28
.= (z1 - z2) + z3 ; ::_thesis: verum
end;

theorem :: SEQ_4:78
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) + z3 = (z1 + z3) - z2 by Th76;

theorem Th79: :: SEQ_4:79
for n being Element of NAT
for z1, z being Element of COMPLEX n holds z1 = (z1 + z) - z
proof
let n be Element of NAT ; ::_thesis: for z1, z being Element of COMPLEX n holds z1 = (z1 + z) - z
let z1, z be Element of COMPLEX n; ::_thesis: z1 = (z1 + z) - z
thus z1 = z1 + (0c n) by BINOP_2:1, FINSEQOP:56
.= z1 + (z - z) by Th73
.= (z1 + z) - z by Th76 ; ::_thesis: verum
end;

theorem Th80: :: SEQ_4:80
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds z1 + (z2 - z1) = z2
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds z1 + (z2 - z1) = z2
let z1, z2 be Element of COMPLEX n; ::_thesis: z1 + (z2 - z1) = z2
thus z1 + (z2 - z1) = (z2 + (- z1)) + z1
.= z2 + ((- z1) + z1) by FINSEQOP:28
.= z2 + (0c n) by Th51, Th52, BINOP_2:1, FINSEQOP:73
.= z2 by BINOP_2:1, FINSEQOP:56 ; ::_thesis: verum
end;

theorem Th81: :: SEQ_4:81
for n being Element of NAT
for z1, z being Element of COMPLEX n holds z1 = (z1 - z) + z
proof
let n be Element of NAT ; ::_thesis: for z1, z being Element of COMPLEX n holds z1 = (z1 - z) + z
let z1, z be Element of COMPLEX n; ::_thesis: z1 = (z1 - z) + z
thus z1 = z1 + (0c n) by BINOP_2:1, FINSEQOP:56
.= z1 + ((- z) + z) by Th51, Th52, BINOP_2:1, FINSEQOP:73
.= (z1 + (- z)) + z by FINSEQOP:28
.= (z1 - z) + z ; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
let c be Element of COMPLEX ;
:: original: *
redefine funcc * z ->  Element of COMPLEX n;
coherence
 c * z is Element of COMPLEX n by FINSEQ_2:113;
end;

theorem Th82: :: SEQ_4:82
for k, n being Element of NAT
for c9, c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c9 = z . k holds
(c * z) . k = c * c9
proof
let k, n be Element of NAT ; ::_thesis: for c9, c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c9 = z . k holds
(c * z) . k = c * c9
let c9, c be Element of COMPLEX ; ::_thesis: for z being Element of COMPLEX n st k in Seg n & c9 = z . k holds
(c * z) . k = c * c9
let z be Element of COMPLEX n; ::_thesis: ( k in Seg n & c9 = z . k implies (c * z) . k = c * c9 )
assume that
A1: k in Seg n and
A2: c9 = z . k ; ::_thesis: (c * z) . k = c * c9
 k in dom (c * z) by A1, Lm4;
hence (c * z) . k = (c multcomplex) . c9 by A2, FUNCT_1:12
.= c * c9 by Lm3 ;
::_thesis: verum
end;

theorem :: SEQ_4:83
for n being Element of NAT
for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z
proof
let n be Element of NAT ; ::_thesis: for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z
let c1, c2 be Element of COMPLEX ; ::_thesis: for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z
let z be Element of COMPLEX n; ::_thesis: c1 * (c2 * z) = (c1 * c2) * z
thus (c1 * c2) * z = (multcomplex [;] ((multcomplex . (c1,c2)),(id COMPLEX))) * z by BINOP_2:def_5
.= (multcomplex [;] (c1,(multcomplex [;] (c2,(id COMPLEX))))) * z by FUNCOP_1:62
.= ((multcomplex [;] (c1,(id COMPLEX))) * (multcomplex [;] (c2,(id COMPLEX)))) * z by FUNCOP_1:55
.= c1 * (c2 * z) by RELAT_1:36 ; ::_thesis: verum
end;

theorem :: SEQ_4:84
for n being Element of NAT
for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)
proof
let n be Element of NAT ; ::_thesis: for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)
let c1, c2 be Element of COMPLEX ; ::_thesis: for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)
let z be Element of COMPLEX n; ::_thesis: (c1 + c2) * z = (c1 * z) + (c2 * z)
set c1M = multcomplex [;] (c1,(id COMPLEX));
set c2M = multcomplex [;] (c2,(id COMPLEX));
thus (c1 + c2) * z = (multcomplex [;] ((addcomplex . (c1,c2)),(id COMPLEX))) * z by BINOP_2:def_3
.= (addcomplex .: ((multcomplex [;] (c1,(id COMPLEX))),(multcomplex [;] (c2,(id COMPLEX))))) * z by Th54, FINSEQOP:35
.= (c1 * z) + (c2 * z) by FUNCOP_1:25 ; ::_thesis: verum
end;

theorem :: SEQ_4:85
for n being Element of NAT
for c being Element of COMPLEX
for z1, z2 being Element of COMPLEX n holds c * (z1 + z2) = (c * z1) + (c * z2) by Th54, FINSEQOP:51, FINSEQOP:54;

theorem :: SEQ_4:86
for n being Element of NAT
for z being Element of COMPLEX n holds 1r * z = z
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n holds 1r * z = z
let z be Element of COMPLEX n; ::_thesis: 1r * z = z
A1: rng z c= COMPLEX ;
thus 1r * z = (id COMPLEX) * z by BINOP_2:6, FINSEQOP:44
.= z by A1, RELAT_1:53 ; ::_thesis: verum
end;

theorem :: SEQ_4:87
for n being Element of NAT
for z being Element of COMPLEX n holds 0c * z = 0c n
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n holds 0c * z = 0c n
let z be Element of COMPLEX n; ::_thesis: 0c * z = 0c n
A1: rng z c= COMPLEX ;
thus 0c * z = multcomplex [;] (0c,((id COMPLEX) * z)) by FUNCOP_1:34
.= multcomplex [;] (0c,z) by A1, RELAT_1:53
.= 0c n by Th51, Th54, BINOP_2:1, FINSEQOP:76 ; ::_thesis: verum
end;

theorem :: SEQ_4:88
for n being Element of NAT
for z being Element of COMPLEX n holds (- 1r) * z = - z ;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
:: original: |.
redefine func abs z ->  Element of n -tuples_on REAL;
correctness
coherence
|.z.| is Element of n -tuples_on REAL;
by FINSEQ_2:113;
end;

theorem Th89: :: SEQ_4:89
for k, n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(abs z) . k = |.c.|
proof
let k, n be Element of NAT ; ::_thesis: for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(abs z) . k = |.c.|
let c be Element of COMPLEX ; ::_thesis: for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(abs z) . k = |.c.|
let z be Element of COMPLEX n; ::_thesis: ( k in Seg n & c = z . k implies (abs z) . k = |.c.| )
assume that
A1: k in Seg n and
A2: c = z . k ; ::_thesis: (abs z) . k = |.c.|
 len (abs z) = n by CARD_1:def_7;
then  k in dom (abs z) by A1, FINSEQ_1:def_3;
hence (abs z) . k = abscomplex . c by A2, FUNCT_1:12
.= |.c.| by Def5 ;
::_thesis: verum
end;

theorem Th90: :: SEQ_4:90
for n being Element of NAT holds abs (0c n) = n |-> 0
proof
let n be Element of NAT ; ::_thesis: abs (0c n) = n |-> 0
thus  abs (0c n) = n |-> (abscomplex . 0c) by FINSEQOP:16
.= n |-> 0 by Def5, COMPLEX1:44 ; ::_thesis: verum
end;

theorem Th91: :: SEQ_4:91
for n being Element of NAT
for z being Element of COMPLEX n holds abs (- z) = abs z
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n holds abs (- z) = abs z
let z be Element of COMPLEX n; ::_thesis: abs (- z) = abs z
now__::_thesis:_for_j_being_Nat_st_j_in_Seg_n_holds_
(abs_(-_z))_._j_=_(abs_z)_._j
let j be Nat; ::_thesis: ( j in Seg n implies (abs (- z)) . j = (abs z) . j )
assume A1: j in Seg n ; ::_thesis: (abs (- z)) . j = (abs z) . j
then reconsider c = z . j, c9 = (- z) . j as Element of COMPLEX by Th57;
thus (abs (- z)) . j = |.c9.| by A1, Th89
.= |.(- c).| by A1, Th60
.= |.c.| by COMPLEX1:52
.= (abs z) . j by A1, Th89 ; ::_thesis: verum
end;
hence  abs (- z) = abs z by FINSEQ_2:119; ::_thesis: verum
end;

theorem Th92: :: SEQ_4:92
for n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)
proof
let n be Element of NAT ; ::_thesis: for c being Element of COMPLEX
for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)
let c be Element of COMPLEX ; ::_thesis: for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)
let z be Element of COMPLEX n; ::_thesis: abs (c * z) = |.c.| * (abs z)
now__::_thesis:_for_j_being_Nat_st_j_in_Seg_n_holds_
(abs_(c_*_z))_._j_=_(|.c.|_*_(abs_z))_._j
let j be Nat; ::_thesis: ( j in Seg n implies (abs (c * z)) . j = (|.c.| * (abs z)) . j )
reconsider w = j as Element of NAT by ORDINAL1:def_12;
assume A1: j in Seg n ; ::_thesis: (abs (c * z)) . j = (|.c.| * (abs z)) . j
then reconsider c9 = z . j, cc = (c * z) . j as Element of COMPLEX by Th57;
reconsider ac = (abs z) . w as Real ;
thus (abs (c * z)) . j = |.cc.| by A1, Th89
.= |.(c * c9).| by A1, Th82
.= |.c.| * |.c9.| by COMPLEX1:65
.= |.c.| * ac by A1, Th89
.= (|.c.| * (abs z)) . j by RVSUM_1:45 ; ::_thesis: verum
end;
hence  abs (c * z) = |.c.| * (abs z) by FINSEQ_2:119; ::_thesis: verum
end;

definition
let z be FinSequence of COMPLEX ;
func|.z.| ->  Real equals :: SEQ_4:def 13
 sqrt (Sum (sqr (abs z)));
correctness
coherence
sqrt (Sum (sqr (abs z))) is Real;
;
end;

:: deftheorem  defines |. SEQ_4:def_13_:_
 for z being FinSequence of COMPLEX holds |.z.| = sqrt (Sum (sqr (abs z)));

theorem Th93: :: SEQ_4:93
for n being Element of NAT holds |.(0c n).| = 0
proof
let n be Element of NAT ; ::_thesis: |.(0c n).| = 0
thus |.(0c n).| = sqrt (Sum (sqr (n |-> 0))) by Th90
.= sqrt (Sum (n |-> (0 ^2))) by RVSUM_1:56
.= sqrt (n * 0) by RVSUM_1:80
.= 0 by SQUARE_1:17 ; ::_thesis: verum
end;

theorem Th94: :: SEQ_4:94
for n being Element of NAT
for z being Element of COMPLEX n st |.z.| = 0 holds
z = 0c n
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n st |.z.| = 0 holds
z = 0c n
let z be Element of COMPLEX n; ::_thesis: ( |.z.| = 0 implies z = 0c n )
assume A1: |.z.| = 0 ; ::_thesis: z = 0c n
now__::_thesis:_for_j_being_Nat_st_j_in_Seg_n_holds_
z_._j_=_(n_|->_0c)_._j
let j be Nat; ::_thesis: ( j in Seg n implies z . j = (n |-> 0c) . j )
assume A2: j in Seg n ; ::_thesis: z . j = (n |-> 0c) . j
then reconsider c = z . j as Element of COMPLEX by Th57;
 0 <= Sum (sqr (abs z)) by RVSUM_1:86;
then  (abs z) . j = (n |-> 0) . j by A1, RVSUM_1:91, SQUARE_1:24;
then  |.c.| = (n |-> 0) . j by A2, Th89;
then  c = 0c by COMPLEX1:45;
hence  z . j = (n |-> 0c) . j ; ::_thesis: verum
end;
hence  z = 0c n by FINSEQ_2:119; ::_thesis: verum
end;

theorem Th95: :: SEQ_4:95
for n being Element of NAT
for z being Element of COMPLEX n holds 0 <= |.z.|
proof
let n be Element of NAT ; ::_thesis: for z being Element of COMPLEX n holds 0 <= |.z.|
let z be Element of COMPLEX n; ::_thesis: 0 <= |.z.|
 0 <= Sum (sqr (abs z)) by RVSUM_1:86;
hence  0 <= |.z.| by SQUARE_1:def_2; ::_thesis: verum
end;

theorem :: SEQ_4:96
for n being Element of NAT
for z being Element of COMPLEX n holds |.(- z).| = |.z.| by Th91;

theorem :: SEQ_4:97
for n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|
proof
let n be Element of NAT ; ::_thesis: for c being Element of COMPLEX
for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|
let c be Element of COMPLEX ; ::_thesis: for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|
let z be Element of COMPLEX n; ::_thesis: |.(c * z).| = |.c.| * |.z.|
A1: ( 0 <= |.c.| ^2 & 0 <= Sum (sqr (abs z)) ) by RVSUM_1:86, XREAL_1:63;
thus |.(c * z).| = sqrt (Sum (sqr (|.c.| * (abs z)))) by Th92
.= sqrt (Sum ((|.c.| ^2) * (sqr (abs z)))) by RVSUM_1:58
.= sqrt ((|.c.| ^2) * (Sum (sqr (abs z)))) by RVSUM_1:87
.= (sqrt (|.c.| ^2)) * (sqrt (Sum (sqr (abs z)))) by A1, SQUARE_1:29
.= |.c.| * |.z.| by COMPLEX1:46, SQUARE_1:22 ; ::_thesis: verum
end;

theorem Th98: :: SEQ_4:98
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 + z2).| <= |.z1.| + |.z2.|
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds |.(z1 + z2).| <= |.z1.| + |.z2.|
let z1, z2 be Element of COMPLEX n; ::_thesis: |.(z1 + z2).| <= |.z1.| + |.z2.|
A1: 0 <= Sum (sqr (abs (z1 + z2))) by RVSUM_1:86;
A2: 0 <= Sum (sqr (abs z1)) by RVSUM_1:86;
then A3: 0 <= sqrt (Sum (sqr (abs z1))) by SQUARE_1:def_2;
A4: for k being Nat st k in Seg n holds
0 <= (mlt ((abs z1),(abs z2))) . k
proof
let k be Nat; ::_thesis: ( k in Seg n implies 0 <= (mlt ((abs z1),(abs z2))) . k )
set r = (mlt ((abs z1),(abs z2))) . k;
assume A5: k in Seg n ; ::_thesis: 0 <= (mlt ((abs z1),(abs z2))) . k
then reconsider c1 = z1 . k, c2 = z2 . k as Element of COMPLEX by Th57;
 ( (abs z1) . k = |.c1.| & (abs z2) . k = |.c2.| ) by A5, Th89;
then A6: (mlt ((abs z1),(abs z2))) . k = |.c1.| * |.c2.| by RVSUM_1:60;
 ( 0 <= |.c1.| & 0 <= |.c2.| ) by COMPLEX1:46;
hence  0 <= (mlt ((abs z1),(abs z2))) . k by A6; ::_thesis: verum
end;
 0 <= (Sum (mlt ((abs z1),(abs z2)))) ^2 by XREAL_1:63;
then A7: sqrt ((Sum (mlt ((abs z1),(abs z2)))) ^2) <= sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2)))) by RVSUM_1:92, SQUARE_1:26;
 len (mlt ((abs z1),(abs z2))) = n by CARD_1:def_7;
then  dom (mlt ((abs z1),(abs z2))) = Seg n by FINSEQ_1:def_3;
then  Sum (mlt ((abs z1),(abs z2))) <= sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2)))) by A4, A7, RVSUM_1:84, SQUARE_1:22;
then  2 * (Sum (mlt ((abs z1),(abs z2)))) <= 2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2))))) by XREAL_1:64;
then  (Sum (sqr (abs z1))) + (2 * (Sum (mlt ((abs z1),(abs z2))))) <= (Sum (sqr (abs z1))) + (2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2)))))) by XREAL_1:7;
then A8: ((Sum (sqr (abs z1))) + (2 * (Sum (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) <= ((Sum (sqr (abs z1))) + (2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2))))))) + (Sum (sqr (abs z2))) by XREAL_1:7;
A9: for k being Nat st k in Seg n holds
(sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k
proof
let k be Nat; ::_thesis: ( k in Seg n implies (sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k )
set r2 = (sqr ((abs z1) + (abs z2))) . k;
 len ((abs z1) + (abs z2)) = n by CARD_1:def_7;
then A10: dom ((abs z1) + (abs z2)) = Seg n by FINSEQ_1:def_3;
assume A11: k in Seg n ; ::_thesis: (sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k
then reconsider c12 = (z1 + z2) . k as Element of COMPLEX by Th57;
reconsider abs912 = (abs (z1 + z2)) . k as Real ;
 0 <= |.c12.| by COMPLEX1:46;
then A12: 0 <= abs912 by A11, Th89;
reconsider abs1 = (abs z1) . k, abs2 = (abs z2) . k as Real ;
reconsider c1 = z1 . k, c2 = z2 . k as Element of COMPLEX by A11, Th57;
reconsider abs12 = ((abs z1) + (abs z2)) . k as Real ;
 |.(c1 + c2).| <= |.c1.| + |.c2.| by COMPLEX1:56;
then  |.c12.| <= |.c1.| + |.c2.| by A11, Th58;
then  |.c12.| <= |.c1.| + abs2 by A11, Th89;
then  |.c12.| <= abs1 + abs2 by A11, Th89;
then  |.c12.| <= abs12 by A11, A10, VALUED_1:def_1;
then  abs912 <= abs12 by A11, Th89;
then  abs912 ^2 <= abs12 ^2 by A12, SQUARE_1:15;
then  abs912 ^2 <= (sqr ((abs z1) + (abs z2))) . k by VALUED_1:11;
hence  (sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k by VALUED_1:11; ::_thesis: verum
end;
A13: 0 <= Sum (sqr (abs z2)) by RVSUM_1:86;
then A14: 0 <= sqrt (Sum (sqr (abs z2))) by SQUARE_1:def_2;
A15: Sum (sqr (abs z1)) = (sqrt (Sum (sqr (abs z1)))) ^2 by A2, SQUARE_1:def_2;
A16: (sqrt (Sum (sqr (abs z2)))) ^2 = Sum (sqr (abs z2)) by A13, SQUARE_1:def_2;
Sum (sqr ((abs z1) + (abs z2))) = Sum (((sqr (abs z1)) + (2 * (mlt ((abs z1),(abs z2))))) + (sqr (abs z2))) by RVSUM_1:68
.= (Sum ((sqr (abs z1)) + (2 * (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) by RVSUM_1:89
.= ((Sum (sqr (abs z1))) + (Sum (2 * (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) by RVSUM_1:89
.= ((Sum (sqr (abs z1))) + (2 * (Sum (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) by RVSUM_1:87 ;
then  Sum (sqr (abs (z1 + z2))) <= ((Sum (sqr (abs z1))) + (2 * (Sum (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) by A9, RVSUM_1:82;
then  Sum (sqr (abs (z1 + z2))) <= ((Sum (sqr (abs z1))) + (2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2))))))) + (Sum (sqr (abs z2))) by A8, XXREAL_0:2;
then  Sum (sqr (abs (z1 + z2))) <= ((Sum (sqr (abs z1))) + (2 * ((sqrt (Sum (sqr (abs z1)))) * (sqrt (Sum (sqr (abs z2))))))) + (Sum (sqr (abs z2))) by A2, A13, SQUARE_1:29;
then  sqrt (Sum (sqr (abs (z1 + z2)))) <= sqrt (((sqrt (Sum (sqr (abs z1)))) + (sqrt (Sum (sqr (abs z2))))) ^2) by A15, A16, A1, SQUARE_1:26;
hence  |.(z1 + z2).| <= |.z1.| + |.z2.| by A3, A14, SQUARE_1:22; ::_thesis: verum
end;

theorem Th99: :: SEQ_4:99
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.|
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.|
let z1, z2 be Element of COMPLEX n; ::_thesis: |.(z1 - z2).| <= |.z1.| + |.z2.|
 |.(z1 - z2).| <= |.z1.| + |.(- z2).| by Th98;
hence  |.(z1 - z2).| <= |.z1.| + |.z2.| by Th91; ::_thesis: verum
end;

theorem :: SEQ_4:100
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 + z2).|
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 + z2).|
let z1, z2 be Element of COMPLEX n; ::_thesis: |.z1.| - |.z2.| <= |.(z1 + z2).|
 z1 = (z1 + z2) - z2 by Th79;
then  |.z1.| <= |.(z1 + z2).| + |.z2.| by Th99;
hence  |.z1.| - |.z2.| <= |.(z1 + z2).| by XREAL_1:20; ::_thesis: verum
end;

theorem :: SEQ_4:101
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 - z2).|
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 - z2).|
let z1, z2 be Element of COMPLEX n; ::_thesis: |.z1.| - |.z2.| <= |.(z1 - z2).|
 z1 = (z1 - z2) + z2 by Th81;
then  |.z1.| <= |.(z1 - z2).| + |.z2.| by Th98;
hence  |.z1.| - |.z2.| <= |.(z1 - z2).| by XREAL_1:20; ::_thesis: verum
end;

theorem Th102: :: SEQ_4:102
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
let z1, z2 be Element of COMPLEX n; ::_thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 )
thus  ( |.(z1 - z2).| = 0 implies z1 = z2 ) ::_thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 )
proof
assume  |.(z1 - z2).| = 0 ; ::_thesis: z1 = z2
then  z1 - z2 = 0c n by Th94;
hence  z1 = z2 by Th74; ::_thesis: verum
end;
assume  z1 = z2 ; ::_thesis: |.(z1 - z2).| = 0
then  z1 - z2 = 0c n by Th73;
hence  |.(z1 - z2).| = 0 by Th93; ::_thesis: verum
end;

theorem :: SEQ_4:103
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 <> z2 holds
0 < |.(z1 - z2).|
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n st z1 <> z2 holds
0 < |.(z1 - z2).|
let z1, z2 be Element of COMPLEX n; ::_thesis: ( z1 <> z2 implies 0 < |.(z1 - z2).| )
assume  z1 <> z2 ; ::_thesis: 0 < |.(z1 - z2).|
then  0 <> |.(z1 - z2).| by Th102;
hence  0 < |.(z1 - z2).| by Th95; ::_thesis: verum
end;

theorem Th104: :: SEQ_4:104
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| = |.(z2 - z1).|
proof
let n be Element of NAT ; ::_thesis: for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| = |.(z2 - z1).|
let z1, z2 be Element of COMPLEX n; ::_thesis: |.(z1 - z2).| = |.(z2 - z1).|
thus |.(z1 - z2).| = |.(- (z2 - z1)).| by Th71
.= |.(z2 - z1).| by Th91 ; ::_thesis: verum
end;

theorem Th105: :: SEQ_4:105
for n being Element of NAT
for z1, z2, z being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
proof
let n be Element of NAT ; ::_thesis: for z1, z2, z being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
let z1, z2, z be Element of COMPLEX n; ::_thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
|.(z1 - z2).| = |.(((z1 - z) + z) - z2).| by Th81
.= |.((z1 - z) + (z - z2)).| by Th76 ;
hence  |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by Th98; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
attrA is open  means :Def14: :: SEQ_4:def 14
 for x being Element of COMPLEX n st x in A holds
ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) );
end;

:: deftheorem Def14 defines open SEQ_4:def_14_:_
 for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is open iff for x being Element of COMPLEX n st x in A holds
ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) );

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
attrA is closed  means :: SEQ_4:def 15
 for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A;
end;

:: deftheorem  defines closed SEQ_4:def_15_:_
 for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is closed iff for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A );

theorem :: SEQ_4:106
for n being Element of NAT
for A being Subset of (COMPLEX n) st A = {} holds
A is open
proof
let n be Element of NAT ; ::_thesis: for A being Subset of (COMPLEX n) st A = {} holds
A is open
let A be Subset of (COMPLEX n); ::_thesis: ( A = {} implies A is open )
assume A1: A = {} ; ::_thesis: A is open
let x be Element of COMPLEX n; :: according to SEQ_4:def_14 ::_thesis: ( x in A implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) )
thus  ( x in A implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) ) by A1; ::_thesis: verum
end;

theorem :: SEQ_4:107
for n being Element of NAT
for A being Subset of (COMPLEX n) st A = COMPLEX n holds
A is open
proof
let n be Element of NAT ; ::_thesis: for A being Subset of (COMPLEX n) st A = COMPLEX n holds
A is open
let A be Subset of (COMPLEX n); ::_thesis: ( A = COMPLEX n implies A is open )
assume A1: A = COMPLEX n ; ::_thesis: A is open
let x be Element of COMPLEX n; :: according to SEQ_4:def_14 ::_thesis: ( x in A implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) )
assume  x in A ; ::_thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) )
take j = 1; ::_thesis: ( 0 < j & ( for z being Element of COMPLEX n st |.z.| < j holds
x + z in A ) )
thus  0 < j ; ::_thesis: for z being Element of COMPLEX n st |.z.| < j holds
x + z in A
let z be Element of COMPLEX n; ::_thesis: ( |.z.| < j implies x + z in A )
assume  |.z.| < j ; ::_thesis: x + z in A
thus  x + z in A by A1; ::_thesis: verum
end;

theorem :: SEQ_4:108
for n being Element of NAT
for AA being Subset-Family of (COMPLEX n) st ( for A being Subset of (COMPLEX n) st A in AA holds
A is open ) holds
for A being Subset of (COMPLEX n) st A = union AA holds
A is open
proof
let n be Element of NAT ; ::_thesis: for AA being Subset-Family of (COMPLEX n) st ( for A being Subset of (COMPLEX n) st A in AA holds
A is open ) holds
for A being Subset of (COMPLEX n) st A = union AA holds
A is open
let AA be Subset-Family of (COMPLEX n); ::_thesis: ( ( for A being Subset of (COMPLEX n) st A in AA holds
A is open ) implies for A being Subset of (COMPLEX n) st A = union AA holds
A is open )
assume A1: for A being Subset of (COMPLEX n) st A in AA holds
A is open ; ::_thesis: for A being Subset of (COMPLEX n) st A = union AA holds
A is open
let A be Subset of (COMPLEX n); ::_thesis: ( A = union AA implies A is open )
assume A2: A = union AA ; ::_thesis: A is open
let x be Element of COMPLEX n; :: according to SEQ_4:def_14 ::_thesis: ( x in A implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) )
assume  x in A ; ::_thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) )
then consider B being set  such that
A3: x in B and
A4: B in AA by A2, TARSKI:def_4;
reconsider B = B as Subset of (COMPLEX n) by A4;
 B is open by A1, A4;
then consider r being Real such that
A5: 0 < r and
A6: for z being Element of COMPLEX n st |.z.| < r holds
x + z in B by A3, Def14;
take  r ; ::_thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) )
thus  0 < r by A5; ::_thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in A
let z be Element of COMPLEX n; ::_thesis: ( |.z.| < r implies x + z in A )
assume  |.z.| < r ; ::_thesis: x + z in A
then  x + z in B by A6;
hence  x + z in A by A2, A4, TARSKI:def_4; ::_thesis: verum
end;

theorem :: SEQ_4:109
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A is open & B is open holds
for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open
proof
let n be Element of NAT ; ::_thesis: for A, B being Subset of (COMPLEX n) st A is open & B is open holds
for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open
let A, B be Subset of (COMPLEX n); ::_thesis: ( A is open & B is open implies for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open )
assume that
A1: A is open and
A2: B is open ; ::_thesis: for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open
let C be Subset of (COMPLEX n); ::_thesis: ( C = A /\ B implies C is open )
assume A3: C = A /\ B ; ::_thesis: C is open
let x be Element of COMPLEX n; :: according to SEQ_4:def_14 ::_thesis: ( x in C implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in C ) ) )
assume A4: x in C ; ::_thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in C ) )
then  x in A by A3, XBOOLE_0:def_4;
then consider r1 being Real such that
A5: 0 < r1 and
A6: for z being Element of COMPLEX n st |.z.| < r1 holds
x + z in A by A1, Def14;
 x in B by A3, A4, XBOOLE_0:def_4;
then consider r2 being Real such that
A7: 0 < r2 and
A8: for z being Element of COMPLEX n st |.z.| < r2 holds
x + z in B by A2, Def14;
take  min (r1,r2) ; ::_thesis: ( 0 < min (r1,r2) & ( for z being Element of COMPLEX n st |.z.| < min (r1,r2) holds
x + z in C ) )
thus  0 < min (r1,r2) by A5, A7, XXREAL_0:15; ::_thesis: for z being Element of COMPLEX n st |.z.| < min (r1,r2) holds
x + z in C
let z be Element of COMPLEX n; ::_thesis: ( |.z.| < min (r1,r2) implies x + z in C )
assume A9: |.z.| < min (r1,r2) ; ::_thesis: x + z in C
 min (r1,r2) <= r2 by XXREAL_0:17;
then  |.z.| < r2 by A9, XXREAL_0:2;
then A10: x + z in B by A8;
 min (r1,r2) <= r1 by XXREAL_0:17;
then  |.z.| < r1 by A9, XXREAL_0:2;
then  x + z in A by A6;
hence  x + z in C by A3, A10, XBOOLE_0:def_4; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let x be Element of COMPLEX n;
let r be Real;
func Ball (x,r) ->  Subset of (COMPLEX n) equals :: SEQ_4:def 16
 {  z where z is Element of COMPLEX n : |.(z - x).| < r  }  ;
coherence
  {  z where z is Element of COMPLEX n : |.(z - x).| < r  }  is Subset of (COMPLEX n)
proof
defpred S1[ FinSequence of COMPLEX ] means |.($1 - x).| < r;
  {  z where z is Element of COMPLEX n : S1[z]  }  c= COMPLEX n from FRAENKEL:sch_10();
hence   {  z where z is Element of COMPLEX n : |.(z - x).| < r  }  is Subset of (COMPLEX n) ; ::_thesis: verum
end;
end;

:: deftheorem  defines Ball SEQ_4:def_16_:_
 for n being Element of NAT
for x being Element of COMPLEX n
for r being Real holds Ball (x,r) =  {  z where z is Element of COMPLEX n : |.(z - x).| < r  }  ;

theorem Th110: :: SEQ_4:110
for n being Element of NAT
for r being Real
for z, x being Element of COMPLEX n holds
( z in Ball (x,r) iff |.(x - z).| < r )
proof
let n be Element of NAT ; ::_thesis: for r being Real
for z, x being Element of COMPLEX n holds
( z in Ball (x,r) iff |.(x - z).| < r )
let r be Real; ::_thesis: for z, x being Element of COMPLEX n holds
( z in Ball (x,r) iff |.(x - z).| < r )
let z, x be Element of COMPLEX n; ::_thesis: ( z in Ball (x,r) iff |.(x - z).| < r )
A1: ( z in  {  z2 where z2 is Element of COMPLEX n : |.(z2 - x).| < r  }  iff ex z1 being Element of COMPLEX n st
( z = z1 & |.(z1 - x).| < r ) ) ;
 |.(z - x).| = |.(x - z).| by Th104;
hence  ( z in Ball (x,r) iff |.(x - z).| < r ) by A1; ::_thesis: verum
end;

theorem :: SEQ_4:111
for n being Element of NAT
for r being Real
for x being Element of COMPLEX n st 0 < r holds
x in Ball (x,r)
proof
let n be Element of NAT ; ::_thesis: for r being Real
for x being Element of COMPLEX n st 0 < r holds
x in Ball (x,r)
let r be Real; ::_thesis: for x being Element of COMPLEX n st 0 < r holds
x in Ball (x,r)
let x be Element of COMPLEX n; ::_thesis: ( 0 < r implies x in Ball (x,r) )
assume A1: 0 < r ; ::_thesis: x in Ball (x,r)
 |.(x - x).| = 0 by Th102;
hence  x in Ball (x,r) by A1; ::_thesis: verum
end;

theorem :: SEQ_4:112
for n being Element of NAT
for r1 being Real
for z1 being Element of COMPLEX n holds Ball (z1,r1) is open
proof
let n be Element of NAT ; ::_thesis: for r1 being Real
for z1 being Element of COMPLEX n holds Ball (z1,r1) is open
let r1 be Real; ::_thesis: for z1 being Element of COMPLEX n holds Ball (z1,r1) is open
let z1 be Element of COMPLEX n; ::_thesis: Ball (z1,r1) is open
let x be Element of COMPLEX n; :: according to SEQ_4:def_14 ::_thesis: ( x in Ball (z1,r1) implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (z1,r1) ) ) )
assume  x in Ball (z1,r1) ; ::_thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (z1,r1) ) )
then A1: |.(z1 - x).| < r1 by Th110;
take r = r1 - |.(z1 - x).|; ::_thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (z1,r1) ) )
thus  0 < r by A1, XREAL_1:50; ::_thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (z1,r1)
let z be Element of COMPLEX n; ::_thesis: ( |.z.| < r implies x + z in Ball (z1,r1) )
assume  |.z.| < r ; ::_thesis: x + z in Ball (z1,r1)
then A2: |.z.| + |.(z1 - x).| < r + |.(z1 - x).| by XREAL_1:6;
 (z1 - x) - z = z1 - (x + z) by Th75;
then  |.(z1 - (x + z)).| <= |.z.| + |.(z1 - x).| by Th99;
then  |.(z1 - (x + z)).| < r + |.(z1 - x).| by A2, XXREAL_0:2;
hence  x + z in Ball (z1,r1) by Th110; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let x be Element of COMPLEX n;
let A be Subset of (COMPLEX n);
func dist (x,A) ->  Real means :Def17: :: SEQ_4:def 17
 for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
it = lower_bound X;
existence
 ex b1 being Real st
for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
b1 = lower_bound X
proof
deffunc H1( Element of COMPLEX n) ->  Real = |.(x - $1).|;
defpred S1[ set ] means $1 in A;
reconsider X =  {  H1(z) where z is Element of COMPLEX n : S1[z]  }  as Subset of REAL from DOMAIN_1:sch_8();
take  lower_bound X ; ::_thesis: for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
lower_bound X = lower_bound X
thus  for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
lower_bound X = lower_bound X ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ( for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
b1 = lower_bound X ) & ( for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
b2 = lower_bound X ) holds
b1 = b2
proof
deffunc H1( Element of COMPLEX n) ->  Real = |.(x - $1).|;
defpred S1[ set ] means $1 in A;
reconsider X =  {  H1(z) where z is Element of COMPLEX n : S1[z]  }  as Subset of REAL from DOMAIN_1:sch_8();
let r1, r2 be Real; ::_thesis: ( ( for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
r1 = lower_bound X ) & ( for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
r2 = lower_bound X ) implies r1 = r2 )
assume that
A1: for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
r1 = lower_bound X and
A2: for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
r2 = lower_bound X ; ::_thesis: r1 = r2
 r1 = lower_bound X by A1;
hence  r1 = r2 by A2; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines dist SEQ_4:def_17_:_
 for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n)
for b4 being Real holds
( b4 = dist (x,A) iff for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
b4 = lower_bound X );

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
let r be Real;
func Ball (A,r) ->  Subset of (COMPLEX n) equals :: SEQ_4:def 18
 {  z where z is Element of COMPLEX n : dist (z,A) < r  }  ;
coherence
  {  z where z is Element of COMPLEX n : dist (z,A) < r  }  is Subset of (COMPLEX n)
proof
defpred S1[ Element of COMPLEX n] means  dist ($1,A) < r;
  {  z where z is Element of COMPLEX n : S1[z]  }  c= COMPLEX n from FRAENKEL:sch_10();
hence   {  z where z is Element of COMPLEX n : dist (z,A) < r  }  is Subset of (COMPLEX n) ; ::_thesis: verum
end;
end;

:: deftheorem  defines Ball SEQ_4:def_18_:_
 for n being Element of NAT
for A being Subset of (COMPLEX n)
for r being Real holds Ball (A,r) =  {  z where z is Element of COMPLEX n : dist (z,A) < r  }  ;

theorem Th113: :: SEQ_4:113
for X being Subset of REAL
for r being Real st X <> {} & ( for r9 being Real st r9 in X holds
r <= r9 ) holds
lower_bound X >= r
proof
let X be Subset of REAL; ::_thesis: for r being Real st X <> {} & ( for r9 being Real st r9 in X holds
r <= r9 ) holds
lower_bound X >= r
let r be Real; ::_thesis: ( X <> {} & ( for r9 being Real st r9 in X holds
r <= r9 ) implies lower_bound X >= r )
assume that
A1: X <> {} and
A2: for r9 being Real st r9 in X holds
r <= r9 ; ::_thesis: lower_bound X >= r
 for r9 being ext-real number st r9 in X holds
r <= r9 by A2;
then  r is LowerBound of X by XXREAL_2:def_2;
then A3: X is bounded_below by XXREAL_2:def_9;
now__::_thesis:_for_r9_being_real_number_st_r9_>_0_holds_
(lower_bound_X)_+_r9_>=_r
let r9 be real number ; ::_thesis: ( r9 > 0 implies (lower_bound X) + r9 >= r )
assume  r9 > 0 ; ::_thesis: (lower_bound X) + r9 >= r
then consider r1 being real number  such that
A4: r1 in X and
A5: r1 < (lower_bound X) + r9 by A1, A3, Def2;
 r <= r1 by A2, A4;
hence  (lower_bound X) + r9 >= r by A5, XXREAL_0:2; ::_thesis: verum
end;
hence  lower_bound X >= r by XREAL_1:41; ::_thesis: verum
end;

theorem Th114: :: SEQ_4:114
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0
proof
let n be Element of NAT ; ::_thesis: for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0
let x be Element of COMPLEX n; ::_thesis: for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0
let A be Subset of (COMPLEX n); ::_thesis: ( A <> {} implies dist (x,A) >= 0 )
defpred S1[ set ] means $1 in A;
deffunc H1( Element of COMPLEX n) ->  Real = |.(x - $1).|;
reconsider X =  {  H1(z) where z is Element of COMPLEX n : S1[z]  }  as Subset of REAL from DOMAIN_1:sch_8();
assume  A <> {} ; ::_thesis: dist (x,A) >= 0
then consider z1 being Element of COMPLEX n such that
A1: z1 in A by SUBSET_1:4;
A2: |.(x - z1).| in X by A1;
A3: now__::_thesis:_for_r9_being_Real_st_r9_in_X_holds_
r9_>=_0
let r9 be Real; ::_thesis: ( r9 in X implies r9 >= 0 )
assume  r9 in X ; ::_thesis: r9 >= 0
then  ex z being Element of COMPLEX n st
( r9 = |.(x - z).| & z in A ) ;
hence  r9 >= 0 by Th95; ::_thesis: verum
end;
 dist (x,A) = lower_bound X by Def17;
hence  dist (x,A) >= 0 by A2, A3, Th113; ::_thesis: verum
end;

theorem Th115: :: SEQ_4:115
for n being Element of NAT
for x, z being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|
proof
let n be Element of NAT ; ::_thesis: for x, z being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|
let x, z be Element of COMPLEX n; ::_thesis: for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|
let A be Subset of (COMPLEX n); ::_thesis: ( A <> {} implies dist ((x + z),A) <= (dist (x,A)) + |.z.| )
defpred S1[ set ] means $1 in A;
deffunc H1( Element of COMPLEX n) ->  Real = |.((x + z) - $1).|;
reconsider Y =  {  H1(z1) where z1 is Element of COMPLEX n : S1[z1]  }  as Subset of REAL from DOMAIN_1:sch_8();
deffunc H2( Element of COMPLEX n) ->  Real = |.(x - $1).|;
A1: Y is bounded_below
proof
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of Y
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Y or 0 <= r )
assume  r in Y ; ::_thesis: 0 <= r
then  ex z1 being Element of COMPLEX n st
( r = |.((x + z) - z1).| & z1 in A ) ;
hence  0 <= r by Th95; ::_thesis: verum
end;
reconsider X =  {  H2(z1) where z1 is Element of COMPLEX n : S1[z1]  }  as Subset of REAL from DOMAIN_1:sch_8();
assume  A <> {} ; ::_thesis: dist ((x + z),A) <= (dist (x,A)) + |.z.|
then consider z2 being Element of COMPLEX n such that
A2: z2 in A by SUBSET_1:4;
A3: dist ((x + z),A) = lower_bound Y by Def17;
A4: now__::_thesis:_for_r9_being_Real_st_r9_in_X_holds_
r9_>=_(dist_((x_+_z),A))_-_|.z.|
let r9 be Real; ::_thesis: ( r9 in X implies r9 >= (dist ((x + z),A)) - |.z.| )
assume  r9 in X ; ::_thesis: r9 >= (dist ((x + z),A)) - |.z.|
then consider z3 being Element of COMPLEX n such that
A5: r9 = |.(x - z3).| and
A6: z3 in A ;
 |.((x + z) - z3).| = |.((x - z3) + z).| by Th76;
then A7: |.((x + z) - z3).| <= r9 + |.z.| by A5, Th98;
 |.((x + z) - z3).| in Y by A6;
then  |.((x + z) - z3).| >= dist ((x + z),A) by A3, A1, Def2;
then  r9 + |.z.| >= dist ((x + z),A) by A7, XXREAL_0:2;
hence  r9 >= (dist ((x + z),A)) - |.z.| by XREAL_1:20; ::_thesis: verum
end;
A8: |.(x - z2).| in X by A2;
 dist (x,A) = lower_bound X by Def17;
then  (dist ((x + z),A)) - |.z.| <= dist (x,A) by A8, A4, Th113;
hence  dist ((x + z),A) <= (dist (x,A)) + |.z.| by XREAL_1:20; ::_thesis: verum
end;

theorem Th116: :: SEQ_4:116
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st x in A holds
dist (x,A) = 0
proof
let n be Element of NAT ; ::_thesis: for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st x in A holds
dist (x,A) = 0
let x be Element of COMPLEX n; ::_thesis: for A being Subset of (COMPLEX n) st x in A holds
dist (x,A) = 0
let A be Subset of (COMPLEX n); ::_thesis: ( x in A implies dist (x,A) = 0 )
defpred S1[ set ] means $1 in A;
deffunc H1( Element of COMPLEX n) ->  Real = |.(x - $1).|;
reconsider X =  {  H1(z) where z is Element of COMPLEX n : S1[z]  }  as Subset of REAL from DOMAIN_1:sch_8();
assume A1: x in A ; ::_thesis: dist (x,A) = 0
then A2: |.(x - x).| in X ;
A3: now__::_thesis:_for_r1_being_real_number_st_0_<_r1_holds_
ex_r_being_real_number_st_
(_r_in_X_&_r_<_0_+_r1_)
reconsider r = |.(x - x).| as real number ;
let r1 be real number ; ::_thesis: ( 0 < r1 implies ex r being real number st
( r in X & r < 0 + r1 ) )
assume A4: 0 < r1 ; ::_thesis: ex r being real number st
( r in X & r < 0 + r1 )
take r = r; ::_thesis: ( r in X & r < 0 + r1 )
thus  r in X by A1; ::_thesis: r < 0 + r1
thus  r < 0 + r1 by A4, Th102; ::_thesis: verum
end;
A5: now__::_thesis:_for_r_being_real_number_st_r_in_X_holds_
0_<=_r
let r be real number ; ::_thesis: ( r in X implies 0 <= r )
assume  r in X ; ::_thesis: 0 <= r
then  ex z being Element of COMPLEX n st
( r = |.(x - z).| & z in A ) ;
hence  0 <= r by Th95; ::_thesis: verum
end;
A6: X is bounded_below
proof
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not x in X or 0 <= x )
thus  ( not x in X or 0 <= x ) by A5; ::_thesis: verum
end;
thus  dist (x,A) = lower_bound X by Def17
.= 0 by A2, A5, A6, A3, Def2 ; ::_thesis: verum
end;

theorem :: SEQ_4:117
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist (x,A) > 0
proof
let n be Element of NAT ; ::_thesis: for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist (x,A) > 0
let x be Element of COMPLEX n; ::_thesis: for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist (x,A) > 0
let A be Subset of (COMPLEX n); ::_thesis: ( not x in A & A <> {} & A is closed implies dist (x,A) > 0 )
assume that
A1: not x in A and
A2: A <> {} and
A3: for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A and
A4: dist (x,A) <= 0 ; :: according to SEQ_4:def_15 ::_thesis: contradiction
A5: dist (x,A) = 0 by A2, A4, Th114;
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_z_being_Element_of_COMPLEX_n_st_
(_|.z.|_<_r_&_x_+_z_in_A_)
deffunc H1( Element of COMPLEX n) ->  Real = |.(x - $1).|;
defpred S1[ set ] means $1 in A;
reconsider X =  {  H1(z) where z is Element of COMPLEX n : S1[z]  }  as Subset of REAL from DOMAIN_1:sch_8();
let r be Real; ::_thesis: ( r > 0 implies ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) )
assume A6: r > 0 ; ::_thesis: ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A )
consider z being Element of COMPLEX n such that
A7: z in A by A2, SUBSET_1:4;
A8: X is bounded_below
proof
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in X or 0 <= r )
assume  r in X ; ::_thesis: 0 <= r
then  ex z being Element of COMPLEX n st
( r = |.(x - z).| & z in A ) ;
hence  0 <= r by Th95; ::_thesis: verum
end;
A9: |.(x - z).| in X by A7;
 ( dist (x,A) = lower_bound X & 0 + r = r ) by Def17;
then consider r9 being real number  such that
A10: r9 in X and
A11: r9 < r by A5, A6, A9, A8, Def2;
consider z1 being Element of COMPLEX n such that
A12: ( r9 = |.(x - z1).| & z1 in A ) by A10;
take z = z1 - x; ::_thesis: ( |.z.| < r & x + z in A )
thus  ( |.z.| < r & x + z in A ) by A11, A12, Th80, Th104; ::_thesis: verum
end;
hence  contradiction by A1, A3; ::_thesis: verum
end;

theorem :: SEQ_4:118
for n being Element of NAT
for z1, x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)
proof
let n be Element of NAT ; ::_thesis: for z1, x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)
let z1, x be Element of COMPLEX n; ::_thesis: for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)
let A be Subset of (COMPLEX n); ::_thesis: ( A <> {} implies |.(z1 - x).| + (dist (x,A)) >= dist (z1,A) )
 x + (z1 - x) = z1 by Th80;
hence  ( A <> {} implies |.(z1 - x).| + (dist (x,A)) >= dist (z1,A) ) by Th115; ::_thesis: verum
end;

theorem Th119: :: SEQ_4:119
for n being Element of NAT
for r being Real
for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )
proof
let n be Element of NAT ; ::_thesis: for r being Real
for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )
let r be Real; ::_thesis: for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )
let z be Element of COMPLEX n; ::_thesis: for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )
let A be Subset of (COMPLEX n); ::_thesis: ( z in Ball (A,r) iff dist (z,A) < r )
 ( z in  {  z2 where z2 is Element of COMPLEX n : dist (z2,A) < r  }  iff ex z1 being Element of COMPLEX n st
( z = z1 & dist (z1,A) < r ) ) ;
hence  ( z in Ball (A,r) iff dist (z,A) < r ) ; ::_thesis: verum
end;

theorem Th120: :: SEQ_4:120
for n being Element of NAT
for r being Real
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball (A,r)
proof
let n be Element of NAT ; ::_thesis: for r being Real
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball (A,r)
let r be Real; ::_thesis: for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball (A,r)
let x be Element of COMPLEX n; ::_thesis: for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball (A,r)
let A be Subset of (COMPLEX n); ::_thesis: ( 0 < r & x in A implies x in Ball (A,r) )
assume that
A1: 0 < r and
A2: x in A ; ::_thesis: x in Ball (A,r)
 dist (x,A) = 0 by A2, Th116;
hence  x in Ball (A,r) by A1; ::_thesis: verum
end;

theorem :: SEQ_4:121
for n being Element of NAT
for r being Real
for A being Subset of (COMPLEX n) st 0 < r holds
A c= Ball (A,r)
proof
let n be Element of NAT ; ::_thesis: for r being Real
for A being Subset of (COMPLEX n) st 0 < r holds
A c= Ball (A,r)
let r be Real; ::_thesis: for A being Subset of (COMPLEX n) st 0 < r holds
A c= Ball (A,r)
let A be Subset of (COMPLEX n); ::_thesis: ( 0 < r implies A c= Ball (A,r) )
assume A1: r > 0 ; ::_thesis: A c= Ball (A,r)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in Ball (A,r) )
assume  x in A ; ::_thesis: x in Ball (A,r)
hence  x in Ball (A,r) by A1, Th120; ::_thesis: verum
end;

theorem :: SEQ_4:122
for n being Element of NAT
for r1 being Real
for A being Subset of (COMPLEX n) st A <> {} holds
Ball (A,r1) is open
proof
let n be Element of NAT ; ::_thesis: for r1 being Real
for A being Subset of (COMPLEX n) st A <> {} holds
Ball (A,r1) is open
let r1 be Real; ::_thesis: for A being Subset of (COMPLEX n) st A <> {} holds
Ball (A,r1) is open
let A be Subset of (COMPLEX n); ::_thesis: ( A <> {} implies Ball (A,r1) is open )
assume A1: A <> {} ; ::_thesis: Ball (A,r1) is open
let x be Element of COMPLEX n; :: according to SEQ_4:def_14 ::_thesis: ( x in Ball (A,r1) implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (A,r1) ) ) )
assume  x in Ball (A,r1) ; ::_thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (A,r1) ) )
then A2: dist (x,A) < r1 by Th119;
take r = r1 - (dist (x,A)); ::_thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (A,r1) ) )
thus  0 < r by A2, XREAL_1:50; ::_thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (A,r1)
let z be Element of COMPLEX n; ::_thesis: ( |.z.| < r implies x + z in Ball (A,r1) )
assume  |.z.| < r ; ::_thesis: x + z in Ball (A,r1)
then A3: |.z.| + (dist (x,A)) < r + (dist (x,A)) by XREAL_1:6;
 dist ((x + z),A) <= |.z.| + (dist (x,A)) by A1, Th115;
then  dist ((x + z),A) < r + (dist (x,A)) by A3, XXREAL_0:2;
hence  x + z in Ball (A,r1) ; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let A, B be Subset of (COMPLEX n);
func dist (A,B) ->  Real means :Def19: :: SEQ_4:def 19
 for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
it = lower_bound X;
existence
 ex b1 being Real st
for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
b1 = lower_bound X
proof
deffunc H1( Element of COMPLEX n, Element of COMPLEX n) ->  Real = |.($1 - $2).|;
defpred S1[ set , set ] means ( $1 in A & $2 in B );
reconsider X =  {  H1(x,z) where x, z is Element of COMPLEX n : S1[x,z]  }  as Subset of REAL from DOMAIN_1:sch_9();
take  lower_bound X ; ::_thesis: for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
lower_bound X = lower_bound X
thus  for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
lower_bound X = lower_bound X ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ( for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
b1 = lower_bound X ) & ( for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
b2 = lower_bound X ) holds
b1 = b2
proof
deffunc H1( Element of COMPLEX n, Element of COMPLEX n) ->  Real = |.($1 - $2).|;
defpred S1[ set , set ] means ( $1 in A & $2 in B );
reconsider X =  {  H1(x,z) where x, z is Element of COMPLEX n : S1[x,z]  }  as Subset of REAL from DOMAIN_1:sch_9();
let r1, r2 be Real; ::_thesis: ( ( for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
r1 = lower_bound X ) & ( for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
r2 = lower_bound X ) implies r1 = r2 )
assume that
A1: for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
r1 = lower_bound X and
A2: for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
r2 = lower_bound X ; ::_thesis: r1 = r2
 r1 = lower_bound X by A1;
hence  r1 = r2 by A2; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines dist SEQ_4:def_19_:_
 for n being Element of NAT
for A, B being Subset of (COMPLEX n)
for b4 being Real holds
( b4 = dist (A,B) iff for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B )  }  holds
b4 = lower_bound X );

theorem :: SEQ_4:123
for X, Y being Subset of REAL st X <> {} & Y <> {} holds
X ++ Y <> {} ;

theorem Th124: :: SEQ_4:124
for X, Y being Subset of REAL st X is bounded_below & Y is bounded_below holds
X ++ Y is bounded_below
proof
let X, Y be Subset of REAL; ::_thesis: ( X is bounded_below & Y is bounded_below implies X ++ Y is bounded_below )
assume  X is bounded_below ; ::_thesis: ( not Y is bounded_below or X ++ Y is bounded_below )
then consider r1 being real number  such that
A1: r1 is LowerBound of X by XXREAL_2:def_9;
A2: for r being real number st r in X holds
r1 <= r by A1, XXREAL_2:def_2;
assume  Y is bounded_below ; ::_thesis: X ++ Y is bounded_below
then consider r2 being real number  such that
A3: r2 is LowerBound of Y by XXREAL_2:def_9;
A4: for r being real number st r in Y holds
r2 <= r by A3, XXREAL_2:def_2;
take  r1 + r2 ; :: according to XXREAL_2:def_9 ::_thesis: r1 + r2 is LowerBound of X ++ Y
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in X ++ Y or r1 + r2 <= r )
assume  r in X ++ Y ; ::_thesis: r1 + r2 <= r
then  r in  {  (r22 + r12) where r22, r12 is Element of COMPLEX : ( r22 in X & r12 in Y )  }  by MEMBER_1:def_6;
then consider r22, r12 being Element of COMPLEX  such that
A5: r = r22 + r12 and
A6: r22 in X and
A7: r12 in Y ;
reconsider r9 = r22, r99 = r12 as real number by A6, A7;
A8: r2 <= r99 by A4, A7;
 r1 <= r9 by A2, A6;
hence  r1 + r2 <= r by A5, A8, XREAL_1:7; ::_thesis: verum
end;

theorem Th125: :: SEQ_4:125
for X, Y being Subset of REAL st X <> {} & X is bounded_below & Y <> {} & Y is bounded_below holds
lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y)
proof
let X, Y be Subset of REAL; ::_thesis: ( X <> {} & X is bounded_below & Y <> {} & Y is bounded_below implies lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y) )
assume that
A1: X <> {} and
A2: X is bounded_below and
A3: Y <> {} and
A4: Y is bounded_below ; ::_thesis: lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y)
A5: now__::_thesis:_for_r9_being_real_number_st_0_<_r9_holds_
ex_r_being_real_number_st_
(_r_in_X_++_Y_&_r_<_((lower_bound_X)_+_(lower_bound_Y))_+_r9_)
let r9 be real number ; ::_thesis: ( 0 < r9 implies ex r being real number st
( r in X ++ Y & r < ((lower_bound X) + (lower_bound Y)) + r9 ) )
assume  0 < r9 ; ::_thesis: ex r being real number st
( r in X ++ Y & r < ((lower_bound X) + (lower_bound Y)) + r9 )
then A6: r9 / 2 > 0 by XREAL_1:215;
then consider r1 being real number  such that
A7: r1 in X and
A8: r1 < (lower_bound X) + (r9 / 2) by A1, A2, Def2;
consider r2 being real number  such that
A9: r2 in Y and
A10: r2 < (lower_bound Y) + (r9 / 2) by A3, A4, A6, Def2;
reconsider r = r1 + r2 as real number ;
take r = r; ::_thesis: ( r in X ++ Y & r < ((lower_bound X) + (lower_bound Y)) + r9 )
thus  r in X ++ Y by A7, A9, MEMBER_1:46; ::_thesis: r < ((lower_bound X) + (lower_bound Y)) + r9
 ((lower_bound X) + (r9 / 2)) + ((lower_bound Y) + (r9 / 2)) = ((lower_bound X) + (lower_bound Y)) + r9 ;
hence  r < ((lower_bound X) + (lower_bound Y)) + r9 by A8, A10, XREAL_1:8; ::_thesis: verum
end;
A11: now__::_thesis:_for_r_being_real_number_st_r_in_X_++_Y_holds_
(lower_bound_X)_+_(lower_bound_Y)_<=_r
let r be real number ; ::_thesis: ( r in X ++ Y implies (lower_bound X) + (lower_bound Y) <= r )
assume  r in X ++ Y ; ::_thesis: (lower_bound X) + (lower_bound Y) <= r
then  r in  {  (r22 + r12) where r22, r12 is Element of COMPLEX : ( r22 in X & r12 in Y )  }  by MEMBER_1:def_6;
then consider r11, r22 being Element of COMPLEX  such that
A12: r = r11 + r22 and
A13: ( r11 in X & r22 in Y ) ;
reconsider r1 = r11, r2 = r22 as real number by A13;
 ( r1 >= lower_bound X & r2 >= lower_bound Y ) by A2, A4, A13, Def2;
hence  (lower_bound X) + (lower_bound Y) <= r by A12, XREAL_1:7; ::_thesis: verum
end;
 ( X ++ Y <> {} & X ++ Y is bounded_below ) by A1, A2, A3, A4, Th124;
hence  lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y) by A11, A5, Def2; ::_thesis: verum
end;

theorem Th126: :: SEQ_4:126
for X, Y being Subset of REAL st Y is bounded_below & X <> {} & ( for r being Real st r in X holds
ex r1 being Real st
( r1 in Y & r1 <= r ) ) holds
lower_bound X >= lower_bound Y
proof
let X, Y be Subset of REAL; ::_thesis: ( Y is bounded_below & X <> {} & ( for r being Real st r in X holds
ex r1 being Real st
( r1 in Y & r1 <= r ) ) implies lower_bound X >= lower_bound Y )
assume that
A1: Y is bounded_below and
A2: X <> {} and
A3: for r being Real st r in X holds
ex r1 being Real st
( r1 in Y & r1 <= r ) ; ::_thesis: lower_bound X >= lower_bound Y
now__::_thesis:_for_r1_being_Real_st_r1_in_X_holds_
r1_>=_lower_bound_Y
let r1 be Real; ::_thesis: ( r1 in X implies r1 >= lower_bound Y )
assume  r1 in X ; ::_thesis: r1 >= lower_bound Y
then consider r2 being Real such that
A4: r2 in Y and
A5: r2 <= r1 by A3;
 lower_bound Y <= r2 by A1, A4, Def2;
hence  r1 >= lower_bound Y by A5, XXREAL_0:2; ::_thesis: verum
end;
hence  lower_bound X >= lower_bound Y by A2, Th113; ::_thesis: verum
end;

theorem Th127: :: SEQ_4:127
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
dist (A,B) >= 0
proof
let n be Element of NAT ; ::_thesis: for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
dist (A,B) >= 0
let A, B be Subset of (COMPLEX n); ::_thesis: ( A <> {} & B <> {} implies dist (A,B) >= 0 )
defpred S1[ set , set ] means ( $1 in A & $2 in B );
deffunc H1( Element of COMPLEX n, Element of COMPLEX n) ->  Real = |.($1 - $2).|;
reconsider Z =  {  H1(z1,z) where z1, z is Element of COMPLEX n : S1[z1,z]  }  as Subset of REAL from DOMAIN_1:sch_9();
assume that
A1: A <> {} and
A2: B <> {} ; ::_thesis: dist (A,B) >= 0
consider z1 being Element of COMPLEX n such that
A3: z1 in A by A1, SUBSET_1:4;
A4: now__::_thesis:_for_r9_being_Real_st_r9_in_Z_holds_
r9_>=_0
let r9 be Real; ::_thesis: ( r9 in Z implies r9 >= 0 )
assume  r9 in Z ; ::_thesis: r9 >= 0
then  ex z1, z being Element of COMPLEX n st
( r9 = |.(z1 - z).| & z1 in A & z in B ) ;
hence  r9 >= 0 by Th95; ::_thesis: verum
end;
consider z2 being Element of COMPLEX n such that
A5: z2 in B by A2, SUBSET_1:4;
A6: dist (A,B) = lower_bound Z by Def19;
 |.(z1 - z2).| in Z by A3, A5;
hence  dist (A,B) >= 0 by A6, A4, Th113; ::_thesis: verum
end;

theorem :: SEQ_4:128
for n being Element of NAT
for A, B being Subset of (COMPLEX n) holds dist (A,B) = dist (B,A)
proof
let n be Element of NAT ; ::_thesis: for A, B being Subset of (COMPLEX n) holds dist (A,B) = dist (B,A)
let A, B be Subset of (COMPLEX n); ::_thesis: dist (A,B) = dist (B,A)
defpred S1[ set , set ] means ( $1 in B & $2 in A );
deffunc H1( Element of COMPLEX n, Element of COMPLEX n) ->  Real = |.($1 - $2).|;
reconsider Y =  {  H1(z,z1) where z, z1 is Element of COMPLEX n : S1[z,z1]  }  as Subset of REAL from DOMAIN_1:sch_9();
defpred S2[ set , set ] means ( $1 in A & $2 in B );
reconsider X =  {  H1(z1,z) where z1, z is Element of COMPLEX n : S2[z1,z]  }  as Subset of REAL from DOMAIN_1:sch_9();
A1: now__::_thesis:_for_r_being_Real_holds_
(_r_in_X_iff_r_in_Y_)
let r be Real; ::_thesis: ( r in X iff r in Y )
A2: now__::_thesis:_(_ex_z,_z1_being_Element_of_COMPLEX_n_st_
(_r_=_|.(z_-_z1).|_&_z_in_B_&_z1_in_A_)_implies_ex_z1,_z_being_Element_of_COMPLEX_n_st_
(_r_=_|.(z1_-_z).|_&_z1_in_A_&_z_in_B_)_)
given z, z1 being Element of COMPLEX n such that A3: ( r = |.(z - z1).| & z in B & z1 in A ) ; ::_thesis: ex z1, z being Element of COMPLEX n st
( r = |.(z1 - z).| & z1 in A & z in B )
take z1 = z1; ::_thesis: ex z being Element of COMPLEX n st
( r = |.(z1 - z).| & z1 in A & z in B )
take z = z; ::_thesis: ( r = |.(z1 - z).| & z1 in A & z in B )
thus  ( r = |.(z1 - z).| & z1 in A & z in B ) by A3, Th104; ::_thesis: verum
end;
now__::_thesis:_(_ex_z1,_z_being_Element_of_COMPLEX_n_st_
(_r_=_|.(z1_-_z).|_&_z1_in_A_&_z_in_B_)_implies_ex_z,_z1_being_Element_of_COMPLEX_n_st_
(_r_=_|.(z_-_z1).|_&_z_in_B_&_z1_in_A_)_)
given z1, z being Element of COMPLEX n such that A4: ( r = |.(z1 - z).| & z1 in A & z in B ) ; ::_thesis: ex z, z1 being Element of COMPLEX n st
( r = |.(z - z1).| & z in B & z1 in A )
take z = z; ::_thesis: ex z1 being Element of COMPLEX n st
( r = |.(z - z1).| & z in B & z1 in A )
take z1 = z1; ::_thesis: ( r = |.(z - z1).| & z in B & z1 in A )
thus  ( r = |.(z - z1).| & z in B & z1 in A ) by A4, Th104; ::_thesis: verum
end;
hence  ( r in X iff r in Y ) by A2; ::_thesis: verum
end;
 ( dist (A,B) = lower_bound X & dist (B,A) = lower_bound Y ) by Def19;
hence  dist (A,B) = dist (B,A) by A1, SUBSET_1:3; ::_thesis: verum
end;

theorem Th129: :: SEQ_4:129
for n being Element of NAT
for x being Element of COMPLEX n
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)
proof
let n be Element of NAT ; ::_thesis: for x being Element of COMPLEX n
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)
let x be Element of COMPLEX n; ::_thesis: for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)
let A, B be Subset of (COMPLEX n); ::_thesis: ( A <> {} & B <> {} implies (dist (x,A)) + (dist (x,B)) >= dist (A,B) )
defpred S1[ set ] means $1 in B;
deffunc H1( Element of COMPLEX n) ->  Real = |.(x - $1).|;
reconsider Y =  {  H1(z) where z is Element of COMPLEX n : S1[z]  }  as Subset of REAL from DOMAIN_1:sch_8();
defpred S2[ set , set ] means ( $1 in A & $2 in B );
defpred S3[ set ] means $1 in A;
deffunc H2( Element of COMPLEX n, Element of COMPLEX n) ->  Real = |.($1 - $2).|;
reconsider X =  {  H1(z) where z is Element of COMPLEX n : S3[z]  }  as Subset of REAL from DOMAIN_1:sch_8();
assume that
A1: A <> {} and
A2: B <> {} ; ::_thesis: (dist (x,A)) + (dist (x,B)) >= dist (A,B)
consider z2 being Element of COMPLEX n such that
A3: z2 in B by A2, SUBSET_1:4;
A4: ( Y <> {} & Y is bounded_below )
proof
 |.(x - z2).| in Y by A3;
hence  Y <> {} ; ::_thesis: Y is bounded_below
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of Y
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Y or 0 <= r )
assume  r in Y ; ::_thesis: 0 <= r
then  ex z1 being Element of COMPLEX n st
( r = |.(x - z1).| & z1 in B ) ;
hence  0 <= r by Th95; ::_thesis: verum
end;
A5: ( lower_bound X = dist (x,A) & lower_bound Y = dist (x,B) ) by Def17;
A6: |.(x - z2).| in Y by A3;
reconsider Z =  {  H2(z1,z) where z1, z is Element of COMPLEX n : S2[z1,z]  }  as Subset of REAL from DOMAIN_1:sch_9();
consider z1 being Element of COMPLEX n such that
A7: z1 in A by A1, SUBSET_1:4;
A8: now__::_thesis:_for_r_being_Real_st_r_in_X_++_Y_holds_
ex_r3_being_Real_st_
(_r3_in_Z_&_r3_<=_r_)
let r be Real; ::_thesis: ( r in X ++ Y implies ex r3 being Real st
( r3 in Z & r3 <= r ) )
assume  r in X ++ Y ; ::_thesis: ex r3 being Real st
( r3 in Z & r3 <= r )
then  r in  {  (r2 + r1) where r2, r1 is Element of COMPLEX : ( r2 in X & r1 in Y )  }  by MEMBER_1:def_6;
then consider r2, r1 being Element of COMPLEX  such that
A9: r = r2 + r1 and
A10: r2 in X and
A11: r1 in Y ;
consider z2 being Element of COMPLEX n such that
A12: ( r1 = |.(x - z2).| & z2 in B ) by A11;
consider z1 being Element of COMPLEX n such that
A13: r2 = |.(x - z1).| and
A14: z1 in A by A10;
take r3 = |.(z1 - z2).|; ::_thesis: ( r3 in Z & r3 <= r )
 r2 = |.(z1 - x).| by A13, Th104;
hence  ( r3 in Z & r3 <= r ) by A9, A14, A12, Th105; ::_thesis: verum
end;
A15: Z is bounded_below
proof
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of Z
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Z or 0 <= r )
assume  r in Z ; ::_thesis: 0 <= r
then  ex z1, z being Element of COMPLEX n st
( r = |.(z1 - z).| & z1 in A & z in B ) ;
hence  0 <= r by Th95; ::_thesis: verum
end;
A16: ( X <> {} & X is bounded_below )
proof
 |.(x - z1).| in X by A7;
hence  X <> {} ; ::_thesis: X is bounded_below
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in X or 0 <= r )
assume  r in X ; ::_thesis: 0 <= r
then  ex z being Element of COMPLEX n st
( r = |.(x - z).| & z in A ) ;
hence  0 <= r by Th95; ::_thesis: verum
end;
A17: lower_bound Z = dist (A,B) by Def19;
A18: X ++ Y c= REAL by MEMBERED:3;
 |.(x - z1).| in X by A7;
then  |.(x - z1).| + |.(x - z2).| in X ++ Y by A6, MEMBER_1:46;
then  lower_bound (X ++ Y) >= lower_bound Z by A15, A8, Th126, A18;
hence  (dist (x,A)) + (dist (x,B)) >= dist (A,B) by A16, A4, A5, A17, Th125; ::_thesis: verum
end;

theorem :: SEQ_4:130
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A meets B holds
dist (A,B) = 0
proof
let n be Element of NAT ; ::_thesis: for A, B being Subset of (COMPLEX n) st A meets B holds
dist (A,B) = 0
let A, B be Subset of (COMPLEX n); ::_thesis: ( A meets B implies dist (A,B) = 0 )
assume  A meets B ; ::_thesis: dist (A,B) = 0
then consider z being set  such that
A1: z in A and
A2: z in B by XBOOLE_0:3;
reconsider z = z as Element of COMPLEX n by A1;
 ( dist (z,A) = 0 & dist (z,B) = 0 ) by A1, A2, Th116;
then  0 + 0 >= dist (A,B) by A1, A2, Th129;
hence  dist (A,B) = 0 by A1, A2, Th127; ::_thesis: verum
end;

definition
let n be Element of NAT ;
func ComplexOpenSets n ->  Subset-Family of (COMPLEX n) equals :: SEQ_4:def 20
 {  A where A is Subset of (COMPLEX n) : A is open  }  ;
coherence
  {  A where A is Subset of (COMPLEX n) : A is open  }  is Subset-Family of (COMPLEX n)
proof
set S =  {  A where A is Subset of (COMPLEX n) : A is open  }  ;
  {  A where A is Subset of (COMPLEX n) : A is open  }  c= bool (COMPLEX n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Subset of (COMPLEX n) : A is open  }  or x in bool (COMPLEX n) )
assume  x in  {  A where A is Subset of (COMPLEX n) : A is open  }  ; ::_thesis: x in bool (COMPLEX n)
then  ex A being Subset of (COMPLEX n) st
( x = A & A is open ) ;
hence  x in bool (COMPLEX n) ; ::_thesis: verum
end;
hence   {  A where A is Subset of (COMPLEX n) : A is open  }  is Subset-Family of (COMPLEX n) ; ::_thesis: verum
end;
end;

:: deftheorem  defines ComplexOpenSets SEQ_4:def_20_:_
 for n being Element of NAT holds ComplexOpenSets n =  {  A where A is Subset of (COMPLEX n) : A is open  }  ;

theorem :: SEQ_4:131
for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A in ComplexOpenSets n iff A is open )
proof
let n be Element of NAT ; ::_thesis: for A being Subset of (COMPLEX n) holds
( A in ComplexOpenSets n iff A is open )
let B be Subset of (COMPLEX n); ::_thesis: ( B in ComplexOpenSets n iff B is open )
 ( B in  {  A where A is Subset of (COMPLEX n) : A is open  }  iff ex C being Subset of (COMPLEX n) st
( B = C & C is open ) ) ;
hence  ( B in ComplexOpenSets n iff B is open ) ; ::_thesis: verum
end;

theorem :: SEQ_4:132
for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is closed iff A ` is open )
proof
let n be Element of NAT ; ::_thesis: for A being Subset of (COMPLEX n) holds
( A is closed iff A ` is open )
let A be Subset of (COMPLEX n); ::_thesis: ( A is closed iff A ` is open )
thus  ( A is closed implies A ` is open ) ::_thesis: ( A ` is open implies A is closed )
proof
assume A1: for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A ; :: according to SEQ_4:def_15 ::_thesis: A ` is open
let x be Element of COMPLEX n; :: according to SEQ_4:def_14 ::_thesis: ( x in A ` implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ` ) ) )
assume  x in A ` ; ::_thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ` ) )
then  not x in A by XBOOLE_0:def_5;
then consider r being Real such that
A2: r > 0 and
A3: for z being Element of COMPLEX n st |.z.| < r holds
not x + z in A by A1;
take  r ; ::_thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ` ) )
thus  0 < r by A2; ::_thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in A `
let z be Element of COMPLEX n; ::_thesis: ( |.z.| < r implies x + z in A ` )
assume  |.z.| < r ; ::_thesis: x + z in A `
hence  x + z in A ` by A3, SUBSET_1:29; ::_thesis: verum
end;
assume A4: for x being Element of COMPLEX n st x in A ` holds
ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ` ) ) ; :: according to SEQ_4:def_14 ::_thesis: A is closed
let x be Element of COMPLEX n; :: according to SEQ_4:def_15 ::_thesis: ( ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) implies x in A )
assume A5: for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ; ::_thesis: x in A
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_z_being_Element_of_COMPLEX_n_st_
(_|.z.|_<_r_&_not_x_+_z_in_A_`_)
let r be Real; ::_thesis: ( r > 0 implies ex z being Element of COMPLEX n st
( |.z.| < r & not x + z in A ` ) )
assume  r > 0 ; ::_thesis: ex z being Element of COMPLEX n st
( |.z.| < r & not x + z in A ` )
then consider z being Element of COMPLEX n such that
A6: ( |.z.| < r & x + z in A ) by A5;
take z = z; ::_thesis: ( |.z.| < r & not x + z in A ` )
thus  ( |.z.| < r & not x + z in A ` ) by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then  not x in A ` by A4;
hence  x in A by SUBSET_1:29; ::_thesis: verum
end;

begin

       defpred S1[ Nat] means  for R being finite Subset of REAL st R <> {} & card R = $1 holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R );

Lm7:  S1[ 0 ]
;

Lm8:  for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A1: S1[n] ; ::_thesis: S1[n + 1]
let R be finite Subset of REAL; ::_thesis: ( R <> {} & card R = n + 1 implies ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R ) )
assume that
A2: R <> {} and
A3: card R = n + 1 ; ::_thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )
now__::_thesis:_(_R_is_bounded_above_&_upper_bound_R_in_R_&_R_is_bounded_below_&_lower_bound_R_in_R_)
percases ( n = 0 or n <> 0 ) ;
supposeA4: n = 0 ; ::_thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )
thus  R is bounded_above ; ::_thesis: ( upper_bound R in R & R is bounded_below & lower_bound R in R )
consider x being set  such that
A5: R = {x} by A3, A4, CARD_2:42;
 x in R by A5, TARSKI:def_1;
then reconsider r = x as Real ;
 upper_bound R = r by A5, Th9;
hence  upper_bound R in R by A5, TARSKI:def_1; ::_thesis: ( R is bounded_below & lower_bound R in R )
thus  R is bounded_below ; ::_thesis: lower_bound R in R
 lower_bound R = r by A5, Th9;
hence  lower_bound R in R by A5, TARSKI:def_1; ::_thesis: verum
end;
supposeA6: n <> 0 ; ::_thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )
set x = the Element of R;
reconsider x = the Element of R as Real by A2, TARSKI:def_3;
reconsider X = R \ {x} as finite Subset of REAL ;
set u = upper_bound X;
set m = max (x,(upper_bound X));
set l = lower_bound X;
set mi = min (x,(lower_bound X));
 {x} c= R by A2, ZFMISC_1:31;
then  card (R \ {x}) = (card R) - (card {x}) by CARD_2:44;
then A7: card X = (n + 1) - 1 by A3, CARD_1:30
.= n ;
then A8: upper_bound X in X by A1, A6, CARD_1:27;
A9: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_s_being_real_number_st_
(_s_in_R_&_(max_(x,(upper_bound_X)))_-_r_<_s_)
reconsider s = max (x,(upper_bound X)) as real number ;
let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st
( s in R & (max (x,(upper_bound X))) - r < s ) )
assume A10: 0 < r ; ::_thesis: ex s being real number st
( s in R & (max (x,(upper_bound X))) - r < s )
take s = s; ::_thesis: ( s in R & (max (x,(upper_bound X))) - r < s )
now__::_thesis:_(_s_in_R_&_(max_(x,(upper_bound_X)))_-_r_<_s_)
percases ( max (x,(upper_bound X)) = x or max (x,(upper_bound X)) = upper_bound X ) by XXREAL_0:16;
suppose max (x,(upper_bound X)) = x ; ::_thesis: ( s in R & (max (x,(upper_bound X))) - r < s )
hence  s in R by A2; ::_thesis: (max (x,(upper_bound X))) - r < s
thus  (max (x,(upper_bound X))) - r < s by A10, XREAL_1:44; ::_thesis: verum
end;
suppose max (x,(upper_bound X)) = upper_bound X ; ::_thesis: ( s in R & (max (x,(upper_bound X))) - r < s )
hence  s in R by A8, XBOOLE_0:def_5; ::_thesis: (max (x,(upper_bound X))) - r < s
thus  (max (x,(upper_bound X))) - r < s by A10, XREAL_1:44; ::_thesis: verum
end;
end;
end;
hence  ( s in R & (max (x,(upper_bound X))) - r < s ) ; ::_thesis: verum
end;
A11: lower_bound X in X by A1, A6, A7, CARD_1:27;
A12: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_s_being_real_number_st_
(_s_in_R_&_s_<_(min_(x,(lower_bound_X)))_+_r_)
reconsider s = min (x,(lower_bound X)) as real number ;
let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st
( s in R & s < (min (x,(lower_bound X))) + r ) )
assume A13: 0 < r ; ::_thesis: ex s being real number st
( s in R & s < (min (x,(lower_bound X))) + r )
take s = s; ::_thesis: ( s in R & s < (min (x,(lower_bound X))) + r )
now__::_thesis:_(_s_in_R_&_s_<_(min_(x,(lower_bound_X)))_+_r_)
percases ( min (x,(lower_bound X)) = x or min (x,(lower_bound X)) = lower_bound X ) by XXREAL_0:15;
suppose min (x,(lower_bound X)) = x ; ::_thesis: ( s in R & s < (min (x,(lower_bound X))) + r )
hence  s in R by A2; ::_thesis: s < (min (x,(lower_bound X))) + r
thus  s < (min (x,(lower_bound X))) + r by A13, XREAL_1:29; ::_thesis: verum
end;
suppose min (x,(lower_bound X)) = lower_bound X ; ::_thesis: ( s in R & s < (min (x,(lower_bound X))) + r )
hence  s in R by A11, XBOOLE_0:def_5; ::_thesis: s < (min (x,(lower_bound X))) + r
thus  s < (min (x,(lower_bound X))) + r by A13, XREAL_1:29; ::_thesis: verum
end;
end;
end;
hence  ( s in R & s < (min (x,(lower_bound X))) + r ) ; ::_thesis: verum
end;
thus  R is bounded_above ; ::_thesis: ( upper_bound R in R & R is bounded_below & lower_bound R in R )
A14: upper_bound X <= max (x,(upper_bound X)) by XXREAL_0:25;
A15: now__::_thesis:_for_s_being_real_number_st_s_in_R_holds_
s_<=_max_(x,(upper_bound_X))
let s be real number ; ::_thesis: ( s in R implies s <= max (x,(upper_bound X)) )
assume A16: s in R ; ::_thesis: s <= max (x,(upper_bound X))
now__::_thesis:_s_<=_max_(x,(upper_bound_X))
percases ( s = x or s <> x ) ;
suppose s = x ; ::_thesis: s <= max (x,(upper_bound X))
hence  s <= max (x,(upper_bound X)) by XXREAL_0:25; ::_thesis: verum
end;
suppose s <> x ; ::_thesis: s <= max (x,(upper_bound X))
then  not s in {x} by TARSKI:def_1;
then  s in X by A16, XBOOLE_0:def_5;
then  s <= upper_bound X by Def1;
hence  s <= max (x,(upper_bound X)) by A14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  s <= max (x,(upper_bound X)) ; ::_thesis: verum
end;
now__::_thesis:_max_(x,(upper_bound_X))_in_R
percases ( max (x,(upper_bound X)) = x or max (x,(upper_bound X)) = upper_bound X ) by XXREAL_0:16;
suppose max (x,(upper_bound X)) = x ; ::_thesis: max (x,(upper_bound X)) in R
hence  max (x,(upper_bound X)) in R by A2; ::_thesis: verum
end;
suppose max (x,(upper_bound X)) = upper_bound X ; ::_thesis: max (x,(upper_bound X)) in R
hence  max (x,(upper_bound X)) in R by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
hence  upper_bound R in R by A15, A9, Def1; ::_thesis: ( R is bounded_below & lower_bound R in R )
thus  R is bounded_below ; ::_thesis: lower_bound R in R
A17: min (x,(lower_bound X)) <= lower_bound X by XXREAL_0:17;
A18: now__::_thesis:_for_s_being_real_number_st_s_in_R_holds_
min_(x,(lower_bound_X))_<=_s
let s be real number ; ::_thesis: ( s in R implies min (x,(lower_bound X)) <= s )
assume A19: s in R ; ::_thesis: min (x,(lower_bound X)) <= s
now__::_thesis:_min_(x,(lower_bound_X))_<=_s
percases ( s = x or s <> x ) ;
suppose s = x ; ::_thesis: min (x,(lower_bound X)) <= s
hence  min (x,(lower_bound X)) <= s by XXREAL_0:17; ::_thesis: verum
end;
suppose s <> x ; ::_thesis: min (x,(lower_bound X)) <= s
then  not s in {x} by TARSKI:def_1;
then  s in X by A19, XBOOLE_0:def_5;
then  lower_bound X <= s by Def2;
hence  min (x,(lower_bound X)) <= s by A17, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  min (x,(lower_bound X)) <= s ; ::_thesis: verum
end;
now__::_thesis:_min_(x,(lower_bound_X))_in_R
percases ( min (x,(lower_bound X)) = x or min (x,(lower_bound X)) = lower_bound X ) by XXREAL_0:15;
suppose min (x,(lower_bound X)) = x ; ::_thesis: min (x,(lower_bound X)) in R
hence  min (x,(lower_bound X)) in R by A2; ::_thesis: verum
end;
suppose min (x,(lower_bound X)) = lower_bound X ; ::_thesis: min (x,(lower_bound X)) in R
hence  min (x,(lower_bound X)) in R by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
hence  lower_bound R in R by A18, A12, Def2; ::_thesis: verum
end;
end;
end;
hence  ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R ) ; ::_thesis: verum
end;

Lm9:  for n being Element of NAT holds S1[n]
from NAT_1:sch_1(Lm7, Lm8);

theorem Th133: :: SEQ_4:133
for R being finite Subset of REAL st R <> {} holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )
proof
let R be finite Subset of REAL; ::_thesis: ( R <> {} implies ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R ) )
assume A1: R <> {} ; ::_thesis: ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )
 S1[ card R] by Lm9;
hence  ( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R ) by A1; ::_thesis: verum
end;

theorem :: SEQ_4:134
for n being Nat
for f being FinSequence holds
( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )
proof
let n be Nat; ::_thesis: for f being FinSequence holds
( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )
let f be FinSequence; ::_thesis: ( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )
thus  ( 1 <= n & n + 1 <= len f implies ( n in dom f & n + 1 in dom f ) ) ::_thesis: ( n in dom f & n + 1 in dom f implies ( 1 <= n & n + 1 <= len f ) )
proof
assume that
A1: 1 <= n and
A2: n + 1 <= len f ; ::_thesis: ( n in dom f & n + 1 in dom f )
 n <= n + 1 by NAT_1:11;
then  ( 1 <= n + 1 & n <= len f ) by A2, NAT_1:11, XXREAL_0:2;
hence  ( n in dom f & n + 1 in dom f ) by A1, A2, FINSEQ_3:25; ::_thesis: verum
end;
thus  ( n in dom f & n + 1 in dom f implies ( 1 <= n & n + 1 <= len f ) ) by FINSEQ_3:25; ::_thesis: verum
end;

theorem :: SEQ_4:135
for n being Nat
for f being FinSequence holds
( 1 <= n & n + 2 <= len f iff ( n in dom f & n + 1 in dom f & n + 2 in dom f ) )
proof
let n be Nat; ::_thesis: for f being FinSequence holds
( 1 <= n & n + 2 <= len f iff ( n in dom f & n + 1 in dom f & n + 2 in dom f ) )
let f be FinSequence; ::_thesis: ( 1 <= n & n + 2 <= len f iff ( n in dom f & n + 1 in dom f & n + 2 in dom f ) )
thus  ( 1 <= n & n + 2 <= len f implies ( n in dom f & n + 1 in dom f & n + 2 in dom f ) ) ::_thesis: ( n in dom f & n + 1 in dom f & n + 2 in dom f implies ( 1 <= n & n + 2 <= len f ) )
proof
assume that
A1: 1 <= n and
A2: n + 2 <= len f ; ::_thesis: ( n in dom f & n + 1 in dom f & n + 2 in dom f )
 n + 1 <= (n + 1) + 1 by NAT_1:11;
then A3: ( 1 <= n + 1 & n + 1 <= len f ) by A2, NAT_1:11, XXREAL_0:2;
 n <= n + 2 by NAT_1:11;
then  ( 1 <= n + 2 & n <= len f ) by A1, A2, XXREAL_0:2;
hence  ( n in dom f & n + 1 in dom f & n + 2 in dom f ) by A1, A2, A3, FINSEQ_3:25; ::_thesis: verum
end;
assume that
A4: n in dom f and
 n + 1 in dom f and
A5: n + 2 in dom f ; ::_thesis: ( 1 <= n & n + 2 <= len f )
thus  ( 1 <= n & n + 2 <= len f ) by A4, A5, FINSEQ_3:25; ::_thesis: verum
end;

theorem :: SEQ_4:136
for D being non empty set
for f1, f2 being FinSequence of D
for n being Element of NAT st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
proof
let D be non empty set ; ::_thesis: for f1, f2 being FinSequence of D
for n being Element of NAT st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
let f1, f2 be FinSequence of D; ::_thesis: for n being Element of NAT st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len f2 implies (f1 ^ f2) /. (n + (len f1)) = f2 /. n )
assume that
A1: 1 <= n and
A2: n <= len f2 ; ::_thesis: (f1 ^ f2) /. (n + (len f1)) = f2 /. n
A3: len f1 < n + (len f1) by A1, NAT_1:19;
 len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22;
then A4: n + (len f1) <= len (f1 ^ f2) by A2, XREAL_1:6;
 n + (len f1) >= n by NAT_1:11;
then  n + (len f1) >= 1 by A1, XXREAL_0:2;
hence (f1 ^ f2) /. (n + (len f1)) = (f1 ^ f2) . (n + (len f1)) by A4, FINSEQ_4:15
.= f2 . ((n + (len f1)) - (len f1)) by A3, A4, FINSEQ_1:24
.= f2 /. n by A1, A2, FINSEQ_4:15 ;
::_thesis: verum
end;

theorem :: SEQ_4:137
for v being FinSequence of REAL st v is increasing holds
for n, m being Element of NAT st n in dom v & m in dom v & n <= m holds
v . n <= v . m
proof
let v be FinSequence of REAL ; ::_thesis: ( v is increasing implies for n, m being Element of NAT st n in dom v & m in dom v & n <= m holds
v . n <= v . m )
assume A1: v is increasing ; ::_thesis: for n, m being Element of NAT st n in dom v & m in dom v & n <= m holds
v . n <= v . m
let n, m be Element of NAT ; ::_thesis: ( n in dom v & m in dom v & n <= m implies v . n <= v . m )
assume that
A2: ( n in dom v & m in dom v ) and
A3: n <= m ; ::_thesis: v . n <= v . m
now__::_thesis:_v_._n_<=_v_._m
percases ( n = m or n <> m ) ;
suppose n = m ; ::_thesis: v . n <= v . m
hence  v . n <= v . m ; ::_thesis: verum
end;
suppose n <> m ; ::_thesis: v . n <= v . m
then  n < m by A3, XXREAL_0:1;
hence  v . n <= v . m by A1, A2, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence  v . n <= v . m ; ::_thesis: verum
end;

theorem Th138: :: SEQ_4:138
for v being FinSequence of REAL st v is increasing holds
for n, m being Element of NAT st n in dom v & m in dom v & n <> m holds
v . n <> v . m
proof
let v be FinSequence of REAL ; ::_thesis: ( v is increasing implies for n, m being Element of NAT st n in dom v & m in dom v & n <> m holds
v . n <> v . m )
assume A1: v is increasing ; ::_thesis: for n, m being Element of NAT st n in dom v & m in dom v & n <> m holds
v . n <> v . m
let n, m be Element of NAT ; ::_thesis: ( n in dom v & m in dom v & n <> m implies v . n <> v . m )
assume that
A2: ( n in dom v & m in dom v ) and
A3: n <> m ; ::_thesis: v . n <> v . m
now__::_thesis:_v_._n_<>_v_._m
percases ( n < m or n > m ) by A3, XXREAL_0:1;
suppose n < m ; ::_thesis: v . n <> v . m
hence  v . n <> v . m by A1, A2, SEQM_3:def_1; ::_thesis: verum
end;
suppose n > m ; ::_thesis: v . n <> v . m
hence  v . n <> v . m by A1, A2, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence  v . n <> v . m ; ::_thesis: verum
end;

theorem Th139: :: SEQ_4:139
for v, v1 being FinSequence of REAL
for n being Element of NAT st v is increasing & v1 = v | (Seg n) holds
v1 is increasing
proof
let v, v1 be FinSequence of REAL ; ::_thesis: for n being Element of NAT st v is increasing & v1 = v | (Seg n) holds
v1 is increasing
let n be Element of NAT ; ::_thesis: ( v is increasing & v1 = v | (Seg n) implies v1 is increasing )
assume that
A1: v is increasing and
A2: v1 = v | (Seg n) ; ::_thesis: v1 is increasing
now__::_thesis:_v1_is_increasing
percases ( n <= len v or len v <= n ) ;
suppose n <= len v ; ::_thesis: v1 is increasing
then  Seg n c= Seg (len v) by FINSEQ_1:5;
then A3: Seg n c= dom v by FINSEQ_1:def_3;
then  Seg n = (dom v) /\ (Seg n) by XBOOLE_1:28;
then A4: dom v1 = Seg n by A2, RELAT_1:61;
now__::_thesis:_for_m,_k_being_Element_of_NAT_st_m_in_dom_v1_&_k_in_dom_v1_&_m_<_k_holds_
v1_._m_<_v1_._k
let m, k be Element of NAT ; ::_thesis: ( m in dom v1 & k in dom v1 & m < k implies v1 . m < v1 . k )
assume that
A5: ( m in dom v1 & k in dom v1 ) and
A6: m < k ; ::_thesis: v1 . m < v1 . k
set r = v1 . m;
set s = v1 . k;
 ( v1 . m = v . m & v1 . k = v . k ) by A2, A5, FUNCT_1:47;
hence  v1 . m < v1 . k by A1, A3, A4, A5, A6, SEQM_3:def_1; ::_thesis: verum
end;
hence  v1 is increasing by SEQM_3:def_1; ::_thesis: verum
end;
suppose len v <= n ; ::_thesis: v1 is increasing
hence  v1 is increasing by A1, A2, FINSEQ_2:20; ::_thesis: verum
end;
end;
end;
hence  v1 is increasing ; ::_thesis: verum
end;

defpred S2[ Element of NAT ] means  for v being FinSequence of REAL st card (rng v) = $1 holds
ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing );

Lm10:  S2[ 0 ]
proof
let v be FinSequence of REAL ; ::_thesis: ( card (rng v) = 0 implies ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) )
assume  card (rng v) = 0 ; ::_thesis: ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
then A1: rng v = {} ;
take v1 = v; ::_thesis: ( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
thus  rng v1 = rng v ; ::_thesis: ( len v1 = card (rng v) & v1 is increasing )
thus  len v1 = card (rng v) by A1, RELAT_1:41; ::_thesis: v1 is increasing
 for n, m being Element of NAT st n in dom v1 & m in dom v1 & n < m holds
v1 . n < v1 . m by A1, RELAT_1:38, RELAT_1:41;
hence  v1 is increasing by SEQM_3:def_1; ::_thesis: verum
end;

Lm11:  for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A1: S2[n] ; ::_thesis: S2[n + 1]
let v be FinSequence of REAL ; ::_thesis: ( card (rng v) = n + 1 implies ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) )
assume A2: card (rng v) = n + 1 ; ::_thesis: ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
now__::_thesis:_ex_v1_being_FinSequence_of_REAL_st_
(_rng_v1_=_rng_v_&_len_v1_=_card_(rng_v)_&_v1_is_increasing_)
reconsider R = rng v as finite Subset of REAL ;
set u = upper_bound R;
set X = R \ {(upper_bound R)};
set f = (R \ {(upper_bound R)}) |` v;
 ( Seq ((R \ {(upper_bound R)}) |` v) = ((R \ {(upper_bound R)}) |` v) * (Sgm (dom ((R \ {(upper_bound R)}) |` v))) & rng (Sgm (dom ((R \ {(upper_bound R)}) |` v))) = dom ((R \ {(upper_bound R)}) |` v) ) by FINSEQ_1:50;
then A3: rng (Seq ((R \ {(upper_bound R)}) |` v)) = rng ((R \ {(upper_bound R)}) |` v) by RELAT_1:28
.= R \ {(upper_bound R)} by RELAT_1:89, XBOOLE_1:36 ;
then reconsider f1 = Seq ((R \ {(upper_bound R)}) |` v) as FinSequence of REAL by FINSEQ_1:def_4;
reconsider X = R \ {(upper_bound R)} as finite set ;
 upper_bound R in R by A2, Th133, CARD_1:27;
then A4: {(upper_bound R)} c= R by ZFMISC_1:31;
then A5: card X = (card R) - (card {(upper_bound R)}) by CARD_2:44;
A6: card {(upper_bound R)} = 1 by CARD_1:30;
then consider v2 being FinSequence of REAL  such that
A7: rng v2 = rng f1 and
A8: len v2 = card (rng f1) and
A9: v2 is increasing by A1, A2, A3, A5;
take v1 = v2 ^ <*(upper_bound R)*>; ::_thesis: ( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
thus  rng v1 = X \/ (rng <*(upper_bound R)*>) by A3, A7, FINSEQ_1:31
.= ((rng v) \ {(upper_bound R)}) \/ {(upper_bound R)} by FINSEQ_1:39
.= (rng v) \/ {(upper_bound R)} by XBOOLE_1:39
.= rng v by A4, XBOOLE_1:12 ; ::_thesis: ( len v1 = card (rng v) & v1 is increasing )
thus A10: len v1 = n + (len <*(upper_bound R)*>) by A2, A3, A5, A6, A8, FINSEQ_1:22
.= card (rng v) by A2, FINSEQ_1:39 ; ::_thesis: v1 is increasing
now__::_thesis:_for_k,_m_being_Element_of_NAT_st_k_in_dom_v1_&_m_in_dom_v1_&_k_<_m_holds_
v1_._k_<_v1_._m
let k, m be Element of NAT ; ::_thesis: ( k in dom v1 & m in dom v1 & k < m implies v1 . k < v1 . m )
assume that
A11: k in dom v1 and
A12: m in dom v1 and
A13: k < m ; ::_thesis: v1 . k < v1 . m
A14: 1 <= m by A12, FINSEQ_3:25;
A15: m <= len v1 by A12, FINSEQ_3:25;
set r = v1 . k;
set s = v1 . m;
A16: 1 <= k by A11, FINSEQ_3:25;
A17: k <= len v1 by A11, FINSEQ_3:25;
now__::_thesis:_v1_._k_<_v1_._m
percases ( m = len v1 or m <> len v1 ) ;
supposeA18: m = len v1 ; ::_thesis: v1 . k < v1 . m
 k < len v1 by A13, A15, XXREAL_0:2;
then  k <= len v2 by A2, A3, A5, A6, A8, A10, NAT_1:13;
then A19: k in dom v2 by A16, FINSEQ_3:25;
then  v1 . k = v2 . k by FINSEQ_1:def_7;
then A20: v1 . k in rng v2 by A19, FUNCT_1:def_3;
then  v1 . k in R by A3, A7, XBOOLE_0:def_5;
then A21: v1 . k <= upper_bound R by Def1;
 not v1 . k in {(upper_bound R)} by A3, A7, A20, XBOOLE_0:def_5;
then A22: v1 . k <> upper_bound R by TARSKI:def_1;
 v1 . m = upper_bound R by A2, A3, A5, A6, A8, A10, A18, FINSEQ_1:42;
hence  v1 . k < v1 . m by A21, A22, XXREAL_0:1; ::_thesis: verum
end;
suppose m <> len v1 ; ::_thesis: v1 . k < v1 . m
then  m < len v1 by A15, XXREAL_0:1;
then  m <= len v2 by A2, A3, A5, A6, A8, A10, NAT_1:13;
then A23: m in dom v2 by A14, FINSEQ_3:25;
then A24: v1 . m = v2 . m by FINSEQ_1:def_7;
 k < len v1 by A13, A17, A15, XXREAL_0:1;
then  k <= len v2 by A2, A3, A5, A6, A8, A10, NAT_1:13;
then A25: k in dom v2 by A16, FINSEQ_3:25;
then  v1 . k = v2 . k by FINSEQ_1:def_7;
hence  v1 . k < v1 . m by A9, A13, A25, A23, A24, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence  v1 . k < v1 . m ; ::_thesis: verum
end;
hence  v1 is increasing by SEQM_3:def_1; ::_thesis: verum
end;
hence  ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) ; ::_thesis: verum
end;

Lm12:  for n being Element of NAT holds S2[n]
from NAT_1:sch_1(Lm10, Lm11);

theorem :: SEQ_4:140
for v being FinSequence of REAL ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) by Lm12;

defpred S3[ Element of NAT ] means  for v1, v2 being FinSequence of REAL st len v1 = $1 & len v2 = $1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2;

Lm13:  S3[ 0 ]
proof
let v1, v2 be FinSequence of REAL ; ::_thesis: ( len v1 = 0 & len v2 = 0 & rng v1 = rng v2 & v1 is increasing & v2 is increasing implies v1 = v2 )
assume that
A1: len v1 = 0 and
A2: len v2 = 0 and
 rng v1 = rng v2 and
 v1 is increasing and
 v2 is increasing ; ::_thesis: v1 = v2
 v1 = {} by A1;
hence  v1 = v2 by A2; ::_thesis: verum
end;

Lm14:  for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A1: S3[n] ; ::_thesis: S3[n + 1]
let v1, v2 be FinSequence of REAL ; ::_thesis: ( len v1 = n + 1 & len v2 = n + 1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing implies v1 = v2 )
assume that
A2: len v1 = n + 1 and
A3: len v2 = n + 1 and
A4: rng v1 = rng v2 and
A5: v1 is increasing and
A6: v2 is increasing ; ::_thesis: v1 = v2
reconsider X = rng v1 as Subset of REAL ;
set u = upper_bound X;
 X <> {} by A2, CARD_1:27, RELAT_1:41;
then A7: upper_bound X in X by Th133;
then consider m being Nat such that
A8: m in dom v2 and
A9: v2 . m = upper_bound X by A4, FINSEQ_2:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A10: m <= len v2 by A8, FINSEQ_3:25;
A11: n <= n + 1 by NAT_1:11;
then  Seg n c= Seg (n + 1) by FINSEQ_1:5;
then A12: Seg n = (Seg (n + 1)) /\ (Seg n) by XBOOLE_1:28;
 dom v2 = Seg (len v2) by FINSEQ_1:def_3;
then A13: dom (v2 | (Seg n)) = Seg n by A3, A12, RELAT_1:61;
 dom v1 = Seg (len v1) by FINSEQ_1:def_3;
then A14: dom (v1 | (Seg n)) = Seg n by A2, A12, RELAT_1:61;
then reconsider f1 = v1 | (Seg n), f2 = v2 | (Seg n) as FinSequence by A13, FINSEQ_1:def_2;
 rng f2 c= rng v2 by RELAT_1:70;
then A15: rng f2 c= REAL by XBOOLE_1:1;
 rng f1 c= rng v1 by RELAT_1:70;
then  rng f1 c= REAL by XBOOLE_1:1;
then reconsider f1 = f1, f2 = f2 as FinSequence of REAL by A15, FINSEQ_1:def_4;
consider k being Nat such that
A16: k in dom v1 and
A17: v1 . k = upper_bound X by A7, FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A18: k <= len v1 by A16, FINSEQ_3:25;
A19: 1 <= k by A16, FINSEQ_3:25;
A20: now__::_thesis:_not_k_<>_len_v1
assume  k <> len v1 ; ::_thesis: contradiction
then  k < len v1 by A18, XXREAL_0:1;
then A21: k + 1 <= len v1 by NAT_1:13;
reconsider s = v1 . (k + 1) as Real ;
A22: k < k + 1 by NAT_1:13;
 1 <= k + 1 by A19, NAT_1:13;
then A23: k + 1 in dom v1 by A21, FINSEQ_3:25;
then  v1 . (k + 1) in rng v1 by FUNCT_1:def_3;
then  s <= upper_bound X by Def1;
hence  contradiction by A5, A16, A17, A23, A22, SEQM_3:def_1; ::_thesis: verum
end;
A24: 1 <= m by A8, FINSEQ_3:25;
A25: now__::_thesis:_not_m_<>_len_v2
assume  m <> len v2 ; ::_thesis: contradiction
then  m < len v2 by A10, XXREAL_0:1;
then A26: m + 1 <= len v2 by NAT_1:13;
reconsider s = v2 . (m + 1) as Real ;
A27: m < m + 1 by NAT_1:13;
 1 <= m + 1 by A24, NAT_1:13;
then A28: m + 1 in dom v2 by A26, FINSEQ_3:25;
then  v2 . (m + 1) in rng v2 by FUNCT_1:def_3;
then  s <= upper_bound X by A4, Def1;
hence  contradiction by A6, A8, A9, A28, A27, SEQM_3:def_1; ::_thesis: verum
end;
A29: len f1 = n by A14, FINSEQ_1:def_3;
then A30: dom f1 c= dom v1 by A2, A11, FINSEQ_3:30;
A31: rng f1 = (rng v1) \ {(upper_bound X)}
proof
thus  rng f1 c= (rng v1) \ {(upper_bound X)} :: according to XBOOLE_0:def_10 ::_thesis: (rng v1) \ {(upper_bound X)} c= rng f1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f1 or x in (rng v1) \ {(upper_bound X)} )
assume  x in rng f1 ; ::_thesis: x in (rng v1) \ {(upper_bound X)}
then consider i being Nat such that
A32: i in dom f1 and
A33: f1 . i = x by FINSEQ_2:10;
A34: x = v1 . i by A32, A33, FUNCT_1:47;
A35: v1 . i in rng v1 by A30, A32, FUNCT_1:def_3;
 i <= n by A14, A32, FINSEQ_1:1;
then  i <> n + 1 by NAT_1:13;
then  x <> upper_bound X by A2, A5, A16, A17, A20, A30, A32, A34, Th138;
then  not x in {(upper_bound X)} by TARSKI:def_1;
hence  x in (rng v1) \ {(upper_bound X)} by A34, A35, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng v1) \ {(upper_bound X)} or x in rng f1 )
assume A36: x in (rng v1) \ {(upper_bound X)} ; ::_thesis: x in rng f1
then  x in rng v1 by XBOOLE_0:def_5;
then consider i being Nat such that
A37: i in dom v1 and
A38: v1 . i = x by FINSEQ_2:10;
A39: i <= len v1 by A37, FINSEQ_3:25;
 not x in {(upper_bound X)} by A36, XBOOLE_0:def_5;
then  i <> len v1 by A17, A20, A38, TARSKI:def_1;
then  i < len v1 by A39, XXREAL_0:1;
then A40: i <= len f1 by A2, A29, NAT_1:13;
 1 <= i by A37, FINSEQ_3:25;
then A41: i in dom f1 by A40, FINSEQ_3:25;
then  f1 . i in rng f1 by FUNCT_1:def_3;
hence  x in rng f1 by A38, A41, FUNCT_1:47; ::_thesis: verum
end;
A42: dom v1 = Seg (len v1) by FINSEQ_1:def_3;
A43: now__::_thesis:_for_i_being_Nat_st_i_in_dom_v1_holds_
(f1_^_<*(upper_bound_X)*>)_._i_=_v1_._i
let i be Nat; ::_thesis: ( i in dom v1 implies (f1 ^ <*(upper_bound X)*>) . i = v1 . i )
assume A44: i in dom v1 ; ::_thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
then A45: 1 <= i by A42, FINSEQ_1:1;
A46: i <= (len f1) + 1 by A2, A29, A42, A44, FINSEQ_1:1;
now__::_thesis:_(f1_^_<*(upper_bound_X)*>)_._i_=_v1_._i
percases ( i = (len f1) + 1 or i <> (len f1) + 1 ) ;
suppose i = (len f1) + 1 ; ::_thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
hence  (f1 ^ <*(upper_bound X)*>) . i = v1 . i by A2, A17, A20, A29, FINSEQ_1:42; ::_thesis: verum
end;
suppose i <> (len f1) + 1 ; ::_thesis: (f1 ^ <*(upper_bound X)*>) . i = v1 . i
then  i < (len f1) + 1 by A46, XXREAL_0:1;
then  i <= len f1 by NAT_1:13;
then A47: i in dom f1 by A14, A29, A45, FINSEQ_1:1;
hence (f1 ^ <*(upper_bound X)*>) . i = f1 . i by FINSEQ_1:def_7
.= v1 . i by A47, FUNCT_1:47 ;
::_thesis: verum
end;
end;
end;
hence  (f1 ^ <*(upper_bound X)*>) . i = v1 . i ; ::_thesis: verum
end;
len (f1 ^ <*(upper_bound X)*>) = n + (len <*(upper_bound X)*>) by A29, FINSEQ_1:22
.= len v1 by A2, FINSEQ_1:39 ;
then A48: v1 = f1 ^ <*(upper_bound X)*> by A43, FINSEQ_2:9;
A49: len f2 = n by A13, FINSEQ_1:def_3;
then A50: len (f2 ^ <*(upper_bound X)*>) = n + (len <*(upper_bound X)*>) by FINSEQ_1:22
.= len v2 by A3, FINSEQ_1:39 ;
A51: dom f2 c= dom v2 by A3, A11, A49, FINSEQ_3:30;
A52: rng f2 = (rng v2) \ {(upper_bound X)}
proof
thus  rng f2 c= (rng v2) \ {(upper_bound X)} :: according to XBOOLE_0:def_10 ::_thesis: (rng v2) \ {(upper_bound X)} c= rng f2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f2 or x in (rng v2) \ {(upper_bound X)} )
assume  x in rng f2 ; ::_thesis: x in (rng v2) \ {(upper_bound X)}
then consider i being Nat such that
A53: i in dom f2 and
A54: f2 . i = x by FINSEQ_2:10;
A55: x = v2 . i by A53, A54, FUNCT_1:47;
A56: v2 . i in rng v2 by A51, A53, FUNCT_1:def_3;
 i <= n by A13, A53, FINSEQ_1:1;
then  i <> n + 1 by NAT_1:13;
then  x <> upper_bound X by A3, A6, A8, A9, A25, A51, A53, A55, Th138;
then  not x in {(upper_bound X)} by TARSKI:def_1;
hence  x in (rng v2) \ {(upper_bound X)} by A55, A56, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng v2) \ {(upper_bound X)} or x in rng f2 )
assume A57: x in (rng v2) \ {(upper_bound X)} ; ::_thesis: x in rng f2
then  x in rng v2 by XBOOLE_0:def_5;
then consider i being Nat such that
A58: i in dom v2 and
A59: v2 . i = x by FINSEQ_2:10;
A60: i <= len v2 by A58, FINSEQ_3:25;
 not x in {(upper_bound X)} by A57, XBOOLE_0:def_5;
then  i <> len v2 by A9, A25, A59, TARSKI:def_1;
then  i < len v2 by A60, XXREAL_0:1;
then A61: i <= len f2 by A3, A49, NAT_1:13;
 1 <= i by A58, FINSEQ_3:25;
then A62: i in dom f2 by A61, FINSEQ_3:25;
then  f2 . i in rng f2 by FUNCT_1:def_3;
hence  x in rng f2 by A59, A62, FUNCT_1:47; ::_thesis: verum
end;
A63: dom v2 = Seg (len v2) by FINSEQ_1:def_3;
A64: now__::_thesis:_for_i_being_Nat_st_i_in_dom_v2_holds_
(f2_^_<*(upper_bound_X)*>)_._i_=_v2_._i
let i be Nat; ::_thesis: ( i in dom v2 implies (f2 ^ <*(upper_bound X)*>) . i = v2 . i )
assume A65: i in dom v2 ; ::_thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
then A66: 1 <= i by A63, FINSEQ_1:1;
A67: i <= (len f2) + 1 by A3, A49, A63, A65, FINSEQ_1:1;
now__::_thesis:_(f2_^_<*(upper_bound_X)*>)_._i_=_v2_._i
percases ( i = (len f2) + 1 or i <> (len f2) + 1 ) ;
suppose i = (len f2) + 1 ; ::_thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
hence  (f2 ^ <*(upper_bound X)*>) . i = v2 . i by A3, A9, A25, A49, FINSEQ_1:42; ::_thesis: verum
end;
suppose i <> (len f2) + 1 ; ::_thesis: (f2 ^ <*(upper_bound X)*>) . i = v2 . i
then  i < (len f2) + 1 by A67, XXREAL_0:1;
then  i <= len f2 by NAT_1:13;
then A68: i in dom f2 by A13, A49, A66, FINSEQ_1:1;
hence (f2 ^ <*(upper_bound X)*>) . i = f2 . i by FINSEQ_1:def_7
.= v2 . i by A68, FUNCT_1:47 ;
::_thesis: verum
end;
end;
end;
hence  (f2 ^ <*(upper_bound X)*>) . i = v2 . i ; ::_thesis: verum
end;
 ( f1 is increasing & f2 is increasing ) by A5, A6, Th139;
then  f1 = f2 by A1, A4, A29, A49, A31, A52;
hence  v1 = v2 by A48, A50, A64, FINSEQ_2:9; ::_thesis: verum
end;

Lm15:  for n being Element of NAT holds S3[n]
from NAT_1:sch_1(Lm13, Lm14);

theorem :: SEQ_4:141
for v1, v2 being FinSequence of REAL st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2 by Lm15;

definition
let v be FinSequence of REAL ;
func Incr v ->  increasing FinSequence of REAL  means :Def21: :: SEQ_4:def 21
( rng it = rng v & len it = card (rng v) );
existence
 ex b1 being increasing FinSequence of REAL st
( rng b1 = rng v & len b1 = card (rng v) )
proof
consider v1 being FinSequence of REAL  such that
A1: ( rng v1 = rng v & len v1 = card (rng v) ) and
A2: v1 is increasing by Lm12;
reconsider v1 = v1 as increasing FinSequence of REAL by A2;
take  v1 ; ::_thesis: ( rng v1 = rng v & len v1 = card (rng v) )
thus  ( rng v1 = rng v & len v1 = card (rng v) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being increasing FinSequence of REAL st rng b1 = rng v & len b1 = card (rng v) & rng b2 = rng v & len b2 = card (rng v) holds
b1 = b2 by Lm15;
end;

:: deftheorem Def21 defines Incr SEQ_4:def_21_:_
 for v being FinSequence of REAL
for b2 being increasing FinSequence of REAL holds
( b2 = Incr v iff ( rng b2 = rng v & len b2 = card (rng v) ) );

registration
let v be non empty FinSequence of REAL ;
cluster Incr v ->  non empty increasing ;
coherence
 not Incr v is empty
proof
A1: len (Incr v) = card (rng v) by Def21;
assume  Incr v is empty ; ::_thesis: contradiction
then  rng v = {} by A1;
hence  contradiction ; ::_thesis: verum
end;
end;

registration
cluster non empty complex-membered ext-real-membered real-membered bounded_below bounded_above for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty & b1 is bounded_above & b1 is bounded_below )
proof
reconsider A = {0} as Subset of REAL ;
take  A ; ::_thesis: ( not A is empty & A is bounded_above & A is bounded_below )
thus  not A is empty ; ::_thesis: ( A is bounded_above & A is bounded_below )
thus  A is bounded_above ; ::_thesis: A is bounded_below
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of A
let t be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not t in A or 0 <= t )
assume  t in A ; ::_thesis: 0 <= t
hence  0 <= t ; ::_thesis: verum
end;
end;

theorem :: SEQ_4:142
for A, B being non empty bounded_below Subset of REAL holds lower_bound (A \/ B) = min ((lower_bound A),(lower_bound B))
proof
let A, B be non empty bounded_below Subset of REAL; ::_thesis: lower_bound (A \/ B) = min ((lower_bound A),(lower_bound B))
set r = min ((lower_bound A),(lower_bound B));
A1: min ((lower_bound A),(lower_bound B)) <= lower_bound B by XXREAL_0:17;
A2: for r1 being real number st ( for t being real number st t in A \/ B holds
t >= r1 ) holds
min ((lower_bound A),(lower_bound B)) >= r1
proof
let r1 be real number ; ::_thesis: ( ( for t being real number st t in A \/ B holds
t >= r1 ) implies min ((lower_bound A),(lower_bound B)) >= r1 )
assume A3: for t being real number st t in A \/ B holds
t >= r1 ; ::_thesis: min ((lower_bound A),(lower_bound B)) >= r1
now__::_thesis:_for_t_being_real_number_st_t_in_B_holds_
t_>=_r1
let t be real number ; ::_thesis: ( t in B implies t >= r1 )
assume  t in B ; ::_thesis: t >= r1
then  t in A \/ B by XBOOLE_0:def_3;
hence  t >= r1 by A3; ::_thesis: verum
end;
then A4: lower_bound B >= r1 by Th43;
now__::_thesis:_for_t_being_real_number_st_t_in_A_holds_
t_>=_r1
let t be real number ; ::_thesis: ( t in A implies t >= r1 )
assume  t in A ; ::_thesis: t >= r1
then  t in A \/ B by XBOOLE_0:def_3;
hence  t >= r1 by A3; ::_thesis: verum
end;
then  lower_bound A >= r1 by Th43;
hence  min ((lower_bound A),(lower_bound B)) >= r1 by A4, XXREAL_0:20; ::_thesis: verum
end;
A5: min ((lower_bound A),(lower_bound B)) <= lower_bound A by XXREAL_0:17;
 for t being real number st t in A \/ B holds
t >= min ((lower_bound A),(lower_bound B))
proof
let t be real number ; ::_thesis: ( t in A \/ B implies t >= min ((lower_bound A),(lower_bound B)) )
assume  t in A \/ B ; ::_thesis: t >= min ((lower_bound A),(lower_bound B))
then  ( t in A or t in B ) by XBOOLE_0:def_3;
then  ( lower_bound A <= t or lower_bound B <= t ) by Def2;
hence  t >= min ((lower_bound A),(lower_bound B)) by A5, A1, XXREAL_0:2; ::_thesis: verum
end;
hence  lower_bound (A \/ B) = min ((lower_bound A),(lower_bound B)) by A2, Th44; ::_thesis: verum
end;

theorem :: SEQ_4:143
for A, B being non empty bounded_above Subset of REAL holds upper_bound (A \/ B) = max ((upper_bound A),(upper_bound B))
proof
let A, B be non empty bounded_above Subset of REAL; ::_thesis: upper_bound (A \/ B) = max ((upper_bound A),(upper_bound B))
set r = max ((upper_bound A),(upper_bound B));
A1: max ((upper_bound A),(upper_bound B)) >= upper_bound B by XXREAL_0:25;
A2: for r1 being real number st ( for t being real number st t in A \/ B holds
t <= r1 ) holds
max ((upper_bound A),(upper_bound B)) <= r1
proof
let r1 be real number ; ::_thesis: ( ( for t being real number st t in A \/ B holds
t <= r1 ) implies max ((upper_bound A),(upper_bound B)) <= r1 )
assume A3: for t being real number st t in A \/ B holds
t <= r1 ; ::_thesis: max ((upper_bound A),(upper_bound B)) <= r1
now__::_thesis:_for_t_being_real_number_st_t_in_B_holds_
t_<=_r1
let t be real number ; ::_thesis: ( t in B implies t <= r1 )
assume  t in B ; ::_thesis: t <= r1
then  t in A \/ B by XBOOLE_0:def_3;
hence  t <= r1 by A3; ::_thesis: verum
end;
then A4: upper_bound B <= r1 by Th45;
now__::_thesis:_for_t_being_real_number_st_t_in_A_holds_
t_<=_r1
let t be real number ; ::_thesis: ( t in A implies t <= r1 )
assume  t in A ; ::_thesis: t <= r1
then  t in A \/ B by XBOOLE_0:def_3;
hence  t <= r1 by A3; ::_thesis: verum
end;
then  upper_bound A <= r1 by Th45;
hence  max ((upper_bound A),(upper_bound B)) <= r1 by A4, XXREAL_0:28; ::_thesis: verum
end;
A5: max ((upper_bound A),(upper_bound B)) >= upper_bound A by XXREAL_0:25;
 for t being real number st t in A \/ B holds
t <= max ((upper_bound A),(upper_bound B))
proof
let t be real number ; ::_thesis: ( t in A \/ B implies t <= max ((upper_bound A),(upper_bound B)) )
assume  t in A \/ B ; ::_thesis: t <= max ((upper_bound A),(upper_bound B))
then  ( t in A or t in B ) by XBOOLE_0:def_3;
then  ( upper_bound A >= t or upper_bound B >= t ) by Def1;
hence  t <= max ((upper_bound A),(upper_bound B)) by A5, A1, XXREAL_0:2; ::_thesis: verum
end;
hence  upper_bound (A \/ B) = max ((upper_bound A),(upper_bound B)) by A2, Th46; ::_thesis: verum
end;

theorem :: SEQ_4:144
for R being non empty Subset of REAL
for r0 being real number st ( for r being real number st r in R holds
r <= r0 ) holds
upper_bound R <= r0
proof
let R be non empty Subset of REAL; ::_thesis: for r0 being real number st ( for r being real number st r in R holds
r <= r0 ) holds
upper_bound R <= r0
let r0 be real number ; ::_thesis: ( ( for r being real number st r in R holds
r <= r0 ) implies upper_bound R <= r0 )
assume A1: for r being real number st r in R holds
r <= r0 ; ::_thesis: upper_bound R <= r0
then  for r being ext-real number st r in R holds
r <= r0 ;
then  r0 is UpperBound of R by XXREAL_2:def_1;
then A2: R is bounded_above by XXREAL_2:def_10;
now__::_thesis:_not_upper_bound_R_>_r0
set r1 = (upper_bound R) - r0;
assume  upper_bound R > r0 ; ::_thesis: contradiction
then  (upper_bound R) - r0 > 0 by XREAL_1:50;
then  ex r being real number st
( r in R & (upper_bound R) - ((upper_bound R) - r0) < r ) by A2, Def1;
hence  contradiction by A1; ::_thesis: verum
end;
hence  upper_bound R <= r0 ; ::_thesis: verum
end;