:: REAL_NS1 semantic presentation

begin

 Lm1:  for n being Nat ex ADD being BinOp of (REAL n) st
( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative )
proof
let n be Nat; ::_thesis: ex ADD being BinOp of (REAL n) st
( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative )
deffunc H1( Element of REAL n, Element of REAL n) ->  Element of REAL n = $1 + $2;
consider ADD being BinOp of (REAL n) such that
A1: for a, b being Element of REAL n holds ADD . (a,b) = H1(a,b) from BINOP_1:sch_4();
now__::_thesis:_for_a,_b,_c_being_Element_of_REAL_n_holds_ADD_._(a,(ADD_._(b,c)))_=_ADD_._((ADD_._(a,b)),c)
let a, b, c be Element of REAL n; ::_thesis: ADD . (a,(ADD . (b,c))) = ADD . ((ADD . (a,b)),c)
reconsider a1 = a, b1 = b, c1 = c as Element of n -tuples_on REAL by EUCLID:def_1;
thus ADD . (a,(ADD . (b,c))) = a + (ADD . (b,c)) by A1
.= a + (b + c) by A1
.= (a1 + b1) + c1 by RVSUM_1:15
.= (ADD . (a,b)) + c by A1
.= ADD . ((ADD . (a,b)),c) by A1 ; ::_thesis: verum
end;
then A2: ADD is associative by BINOP_1:def_3;
now__::_thesis:_for_a,_b_being_Element_of_REAL_n_holds_ADD_._(a,b)_=_ADD_._(b,a)
let a, b be Element of REAL n; ::_thesis: ADD . (a,b) = ADD . (b,a)
thus ADD . (a,b) = a + b by A1
.= ADD . (b,a) by A1 ; ::_thesis: verum
end;
then  ADD is commutative by BINOP_1:def_2;
hence  ex ADD being BinOp of (REAL n) st
( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative ) by A1, A2; ::_thesis: verum
end;

definition
let n be Nat;
func Euclid_add n ->  BinOp of (REAL n) means :Def1: :: REAL_NS1:def 1
 for a, b being Element of REAL n holds it . (a,b) = a + b;
existence
 ex b1 being BinOp of (REAL n) st
for a, b being Element of REAL n holds b1 . (a,b) = a + b
proof
consider ADD being BinOp of (REAL n) such that
A1: for a, b being Element of REAL n holds ADD . (a,b) = a + b and
 ( ADD is commutative & ADD is associative ) by Lm1;
take  ADD ; ::_thesis: for a, b being Element of REAL n holds ADD . (a,b) = a + b
thus  for a, b being Element of REAL n holds ADD . (a,b) = a + b by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (REAL n) st ( for a, b being Element of REAL n holds b1 . (a,b) = a + b ) & ( for a, b being Element of REAL n holds b2 . (a,b) = a + b ) holds
b1 = b2
proof
deffunc H1( Element of REAL n, Element of REAL n) ->  Element of REAL n = $1 + $2;
 for o1, o2 being BinOp of (REAL n) st ( for a, b being Element of REAL n holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of REAL n holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2();
hence  for b1, b2 being BinOp of (REAL n) st ( for a, b being Element of REAL n holds b1 . (a,b) = a + b ) & ( for a, b being Element of REAL n holds b2 . (a,b) = a + b ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Euclid_add REAL_NS1:def_1_:_
 for n being Nat
for b2 being BinOp of (REAL n) holds
( b2 = Euclid_add n iff for a, b being Element of REAL n holds b2 . (a,b) = a + b );

registration
let n be Nat;
cluster Euclid_add n ->  commutative associative ;
coherence
 ( Euclid_add n is commutative & Euclid_add n is associative )
proof
 ex ADD being BinOp of (REAL n) st
( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative ) by Lm1;
hence  ( Euclid_add n is commutative & Euclid_add n is associative ) by Def1; ::_thesis: verum
end;
end;

definition
let n be Nat;
func Euclid_mult n ->  Function of [:REAL,(REAL n):],(REAL n) means :Def2: :: REAL_NS1:def 2
 for r being Element of REAL
for x being Element of REAL n holds it . (r,x) = r * x;
existence
 ex b1 being Function of [:REAL,(REAL n):],(REAL n) st
for r being Element of REAL
for x being Element of REAL n holds b1 . (r,x) = r * x
proof
deffunc H1( real number , Element of REAL n) ->  Element of REAL n = $1 * $2;
 ex f being Function of [:REAL,(REAL n):],(REAL n) st
for r being Element of REAL
for x being Element of REAL n holds f . (r,x) = H1(r,x) from BINOP_1:sch_4();
hence  ex b1 being Function of [:REAL,(REAL n):],(REAL n) st
for r being Element of REAL
for x being Element of REAL n holds b1 . (r,x) = r * x ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:REAL,(REAL n):],(REAL n) st ( for r being Element of REAL
for x being Element of REAL n holds b1 . (r,x) = r * x ) & ( for r being Element of REAL
for x being Element of REAL n holds b2 . (r,x) = r * x ) holds
b1 = b2
proof
let mult1, mult2 be Function of [:REAL,(REAL n):],(REAL n); ::_thesis: ( ( for r being Element of REAL
for x being Element of REAL n holds mult1 . (r,x) = r * x ) & ( for r being Element of REAL
for x being Element of REAL n holds mult2 . (r,x) = r * x ) implies mult1 = mult2 )
assume that
A1: for r being Element of REAL
for x being Element of REAL n holds mult1 . (r,x) = r * x and
A2: for r being Element of REAL
for x being Element of REAL n holds mult2 . (r,x) = r * x ; ::_thesis: mult1 = mult2
 for r being Element of REAL
for x being Element of REAL n holds mult1 . (r,x) = mult2 . (r,x)
proof
let r be Element of REAL ; ::_thesis: for x being Element of REAL n holds mult1 . (r,x) = mult2 . (r,x)
let x be Element of REAL n; ::_thesis: mult1 . (r,x) = mult2 . (r,x)
thus mult1 . (r,x) = r * x by A1
.= mult2 . (r,x) by A2 ; ::_thesis: verum
end;
hence  mult1 = mult2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Euclid_mult REAL_NS1:def_2_:_
 for n being Nat
for b2 being Function of [:REAL,(REAL n):],(REAL n) holds
( b2 = Euclid_mult n iff for r being Element of REAL
for x being Element of REAL n holds b2 . (r,x) = r * x );

definition
let n be Nat;
func Euclid_norm n ->  Function of (REAL n),REAL means :Def3: :: REAL_NS1:def 3
 for x being Element of REAL n holds it . x = |.x.|;
existence
 ex b1 being Function of (REAL n),REAL st
for x being Element of REAL n holds b1 . x = |.x.|
proof
deffunc H1( Element of REAL n) ->  Element of REAL = |.$1.|;
consider f being Function of (REAL n),REAL such that
A1: for x being Element of REAL n holds f . x = H1(x) from FUNCT_2:sch_4();
take  f ; ::_thesis: for x being Element of REAL n holds f . x = |.x.|
let x be Element of REAL n; ::_thesis: f . x = |.x.|
thus  f . x = |.x.| by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (REAL n),REAL st ( for x being Element of REAL n holds b1 . x = |.x.| ) & ( for x being Element of REAL n holds b2 . x = |.x.| ) holds
b1 = b2
proof
let f, g be Function of (REAL n),REAL; ::_thesis: ( ( for x being Element of REAL n holds f . x = |.x.| ) & ( for x being Element of REAL n holds g . x = |.x.| ) implies f = g )
assume that
A2: for x being Element of REAL n holds f . x = |.x.| and
A3: for x being Element of REAL n holds g . x = |.x.| ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_REAL_n_holds_f_._x_=_g_._x
let x be Element of REAL n; ::_thesis: f . x = g . x
thus f . x = |.x.| by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Euclid_norm REAL_NS1:def_3_:_
 for n being Nat
for b2 being Function of (REAL n),REAL holds
( b2 = Euclid_norm n iff for x being Element of REAL n holds b2 . x = |.x.| );

definition
let n be Nat;
func REAL-NS n ->  non empty strict NORMSTR  means :Def4: :: REAL_NS1:def 4
( the carrier of it = REAL n & 0. it = 0* n & the addF of it = Euclid_add n & the Mult of it = Euclid_mult n & the normF of it = Euclid_norm n );
existence
 ex b1 being non empty strict NORMSTR st
( the carrier of b1 = REAL n & 0. b1 = 0* n & the addF of b1 = Euclid_add n & the Mult of b1 = Euclid_mult n & the normF of b1 = Euclid_norm n )
proof
take  NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) ; ::_thesis: ( the carrier of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = REAL n & 0. NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = 0* n & the addF of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_add n & the Mult of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_mult n & the normF of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_norm n )
thus  ( the carrier of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = REAL n & 0. NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = 0* n & the addF of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_add n & the Mult of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_mult n & the normF of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_norm n ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict NORMSTR st the carrier of b1 = REAL n & 0. b1 = 0* n & the addF of b1 = Euclid_add n & the Mult of b1 = Euclid_mult n & the normF of b1 = Euclid_norm n & the carrier of b2 = REAL n & 0. b2 = 0* n & the addF of b2 = Euclid_add n & the Mult of b2 = Euclid_mult n & the normF of b2 = Euclid_norm n holds
b1 = b2 ;
end;

:: deftheorem Def4 defines REAL-NS REAL_NS1:def_4_:_
 for n being Nat
for b2 being non empty strict NORMSTR holds
( b2 = REAL-NS n iff ( the carrier of b2 = REAL n & 0. b2 = 0* n & the addF of b2 = Euclid_add n & the Mult of b2 = Euclid_mult n & the normF of b2 = Euclid_norm n ) );

registration
let n be non empty Nat;
cluster REAL-NS n ->  non empty non trivial strict ;
coherence
 not REAL-NS n is trivial
proof
the carrier of (REAL-NS n) = REAL n by Def4
.= the carrier of (TOP-REAL n) by EUCLID:22 ;
hence  not REAL-NS n is trivial ; ::_thesis: verum
end;
end;

theorem Th1: :: REAL_NS1:1
for n being Nat
for x being VECTOR of (REAL-NS n)
for y being Element of REAL n st x = y holds
||.x.|| = |.y.|
proof
let n be Nat; ::_thesis: for x being VECTOR of (REAL-NS n)
for y being Element of REAL n st x = y holds
||.x.|| = |.y.|
let x be VECTOR of (REAL-NS n); ::_thesis: for y being Element of REAL n st x = y holds
||.x.|| = |.y.|
let y be Element of REAL n; ::_thesis: ( x = y implies ||.x.|| = |.y.| )
assume A1: x = y ; ::_thesis: ||.x.|| = |.y.|
thus ||.x.|| = the normF of (REAL-NS n) . x
.= (Euclid_norm n) . y by A1, Def4
.= |.y.| by Def3 ; ::_thesis: verum
end;

theorem Th2: :: REAL_NS1:2
for n being Nat
for x, y being VECTOR of (REAL-NS n)
for a, b being Element of REAL n st x = a & y = b holds
x + y = a + b
proof
let n be Nat; ::_thesis: for x, y being VECTOR of (REAL-NS n)
for a, b being Element of REAL n st x = a & y = b holds
x + y = a + b
let x, y be VECTOR of (REAL-NS n); ::_thesis: for a, b being Element of REAL n st x = a & y = b holds
x + y = a + b
let a, b be Element of REAL n; ::_thesis: ( x = a & y = b implies x + y = a + b )
assume  ( x = a & y = b ) ; ::_thesis: x + y = a + b
hence x + y = (Euclid_add n) . (a,b) by Def4
.= a + b by Def1 ;
::_thesis: verum
end;

theorem Th3: :: REAL_NS1:3
for n being Nat
for x being VECTOR of (REAL-NS n)
for y being Element of REAL n
for a being real number st x = y holds
a * x = a * y
proof
let n be Nat; ::_thesis: for x being VECTOR of (REAL-NS n)
for y being Element of REAL n
for a being real number st x = y holds
a * x = a * y
let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n
for a being real number st x = y holds
a * x = a * y
let y be Element of REAL n; ::_thesis: for a being real number st x = y holds
a * x = a * y
let a be real number ; ::_thesis: ( x = y implies a * x = a * y )
assume A1: x = y ; ::_thesis: a * x = a * y
reconsider a = a as Real by XREAL_0:def_1;
a * x = (Euclid_mult n) . (a,x) by Def4
.= a * y by A1, Def2 ;
hence  a * x = a * y ; ::_thesis: verum
end;

registration
let n be Nat;
cluster REAL-NS n ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ;
coherence
 ( REAL-NS n is reflexive & REAL-NS n is discerning & REAL-NS n is RealNormSpace-like & REAL-NS n is vector-distributive & REAL-NS n is scalar-distributive & REAL-NS n is scalar-associative & REAL-NS n is scalar-unital & REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
proof
reconsider x1 = 0. (REAL-NS n) as Element of REAL n by Def4;
 ( |.x1.| = 0 iff x1 = 0* n ) by EUCLID:7, EUCLID:8;
hence  ||.(0. (REAL-NS n)).|| = 0 by Def4, Th1; :: according to NORMSP_0:def_6 ::_thesis: ( REAL-NS n is discerning & REAL-NS n is RealNormSpace-like & REAL-NS n is vector-distributive & REAL-NS n is scalar-distributive & REAL-NS n is scalar-associative & REAL-NS n is scalar-unital & REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
 for x, y being Point of (REAL-NS n)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
proof
let x, y be Point of (REAL-NS n); ::_thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
thus  ( ||.x.|| = 0 iff x = 0. (REAL-NS n) ) ::_thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
proof
reconsider x1 = x as Element of REAL n by Def4;
 ( |.x1.| = 0 iff x1 = 0* n ) by EUCLID:7, EUCLID:8;
hence  ( ||.x.|| = 0 iff x = 0. (REAL-NS n) ) by Def4, Th1; ::_thesis: verum
end;
thus  ||.(a * x).|| = (abs a) * ||.x.|| ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
proof
reconsider x1 = x as Element of REAL n by Def4;
thus ||.(a * x).|| = |.(a * x1).| by Th1, Th3
.= (abs a) * |.x1.| by EUCLID:11
.= (abs a) * ||.x.|| by Th1 ; ::_thesis: verum
end;
thus  ||.(x + y).|| <= ||.x.|| + ||.y.|| ::_thesis: verum
proof
reconsider x1 = x, y1 = y as Element of REAL n by Def4;
 |.(x1 + y1).| <= |.x1.| + |.y1.| by EUCLID:12;
then A1: |.(x1 + y1).| <= ||.x.|| + |.y1.| by Th1;
 ||.(x + y).|| = |.(x1 + y1).| by Th1, Th2;
hence  ||.(x + y).|| <= ||.x.|| + ||.y.|| by A1, Th1; ::_thesis: verum
end;
end;
hence  ( REAL-NS n is discerning & REAL-NS n is RealNormSpace-like ) by NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: ( REAL-NS n is vector-distributive & REAL-NS n is scalar-distributive & REAL-NS n is scalar-associative & REAL-NS n is scalar-unital & REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
A2: for a, b being real number
for v being VECTOR of (REAL-NS n) holds (a + b) * v = (a * v) + (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of (REAL-NS n) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
let v be VECTOR of (REAL-NS n); ::_thesis: (a + b) * v = (a * v) + (b * v)
 (a + b) * v = (a * v) + (b * v)
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def_1;
A3: ( a * v = a * v1 & b * v = b * v1 ) by Th3;
thus (a + b) * v = (Euclid_mult n) . ((a + b),v) by Def4
.= (a + b) * v2 by Def2
.= (a * v2) + (b * v2) by RVSUM_1:50
.= (a * v) + (b * v) by A3, Th2 ; ::_thesis: verum
end;
hence  (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
A4: for a being real number
for v, w being VECTOR of (REAL-NS n) holds a * (v + w) = (a * v) + (a * w)
proof
let a be real number ; ::_thesis: for v, w being VECTOR of (REAL-NS n) holds a * (v + w) = (a * v) + (a * w)
reconsider a = a as Real by XREAL_0:def_1;
let v, w be VECTOR of (REAL-NS n); ::_thesis: a * (v + w) = (a * v) + (a * w)
 a * (v + w) = (a * v) + (a * w)
proof
reconsider v1 = v, w1 = w as Element of REAL n by Def4;
reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def_1;
A5: ( a * v = a * v1 & a * w = a * w1 ) by Th3;
thus a * (v + w) = (Euclid_mult n) . (a,(v + w)) by Def4
.= (Euclid_mult n) . (a,(v1 + w1)) by Th2
.= a * (v2 + w2) by Def2
.= (a * v2) + (a * w2) by RVSUM_1:51
.= (a * v) + (a * w) by A5, Th2 ; ::_thesis: verum
end;
hence  a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum
end;
A6: for a, b being real number
for v being VECTOR of (REAL-NS n) holds (a * b) * v = a * (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of (REAL-NS n) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
let v be VECTOR of (REAL-NS n); ::_thesis: (a * b) * v = a * (b * v)
 (a * b) * v = a * (b * v)
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def_1;
A7: b * v = b * v1 by Th3;
(a * b) * v = (Euclid_mult n) . ((a * b),v) by Def4
.= (a * b) * v1 by Def2
.= a * (b * v2) by RVSUM_1:49 ;
hence  (a * b) * v = a * (b * v) by A7, Th3; ::_thesis: verum
end;
hence  (a * b) * v = a * (b * v) ; ::_thesis: verum
end;
 for v being VECTOR of (REAL-NS n) holds 1 * v = v
proof
let v be VECTOR of (REAL-NS n); ::_thesis: 1 * v = v
thus  1 * v = v ::_thesis: verum
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def_1;
thus 1 * v = (Euclid_mult n) . (1,v) by Def4
.= 1 * v2 by Def2
.= v by RVSUM_1:52 ; ::_thesis: verum
end;
end;
hence  ( REAL-NS n is vector-distributive & REAL-NS n is scalar-distributive & REAL-NS n is scalar-associative & REAL-NS n is scalar-unital ) by A4, A2, A6, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: ( REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
 for v, w being VECTOR of (REAL-NS n) holds v + w = w + v
proof
let v, w be VECTOR of (REAL-NS n); ::_thesis: v + w = w + v
thus  v + w = w + v ::_thesis: verum
proof
reconsider v1 = v, w1 = w as Element of REAL n by Def4;
thus v + w = (Euclid_add n) . (v,w) by Def4
.= (Euclid_add n) . (w1,v1) by BINOP_1:def_2
.= w + v by Def4 ; ::_thesis: verum
end;
end;
hence  REAL-NS n is Abelian by RLVECT_1:def_2; ::_thesis: ( REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
 for u, v, w being VECTOR of (REAL-NS n) holds (u + v) + w = u + (v + w)
proof
let u, v, w be VECTOR of (REAL-NS n); ::_thesis: (u + v) + w = u + (v + w)
thus  (u + v) + w = u + (v + w) ::_thesis: verum
proof
reconsider u1 = u, v1 = v, w1 = w as Element of REAL n by Def4;
A8: v + w = v1 + w1 by Th2;
thus (u + v) + w = (Euclid_add n) . (( the addF of (REAL-NS n) . (u,v)),w) by Def4
.= (Euclid_add n) . (((Euclid_add n) . (u1,v1)),w1) by Def4
.= (Euclid_add n) . (u1,((Euclid_add n) . (v1,w1))) by BINOP_1:def_3
.= (Euclid_add n) . (u1,(v1 + w1)) by Def1
.= u1 + (v1 + w1) by Def1
.= u + (v + w) by A8, Th2 ; ::_thesis: verum
end;
end;
hence  REAL-NS n is add-associative by RLVECT_1:def_3; ::_thesis: ( REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
 for v being VECTOR of (REAL-NS n) holds v + (0. (REAL-NS n)) = v
proof
let v be VECTOR of (REAL-NS n); ::_thesis: v + (0. (REAL-NS n)) = v
thus  v + (0. (REAL-NS n)) = v ::_thesis: verum
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def_1;
reconsider zero = n |-> 0 as Element of n -tuples_on REAL by FINSEQ_2:112;
 0. (REAL-NS n) = 0* n by Def4;
hence v + (0. (REAL-NS n)) = v1 + (0* n) by Th2
.= v2 + zero by EUCLID:def_4
.= v by RVSUM_1:16 ;
::_thesis: verum
end;
end;
hence  REAL-NS n is right_zeroed by RLVECT_1:def_4; ::_thesis: REAL-NS n is right_complementable
 REAL-NS n is right_complementable
proof
let v be VECTOR of (REAL-NS n); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
thus  ex w being VECTOR of (REAL-NS n) st v + w = 0. (REAL-NS n) :: according to ALGSTR_0:def_11 ::_thesis: verum
proof
reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def_1;
A9: 0. (REAL-NS n) = 0* n by Def4
.= n |-> 0 by EUCLID:def_4 ;
reconsider w = - v1 as VECTOR of (REAL-NS n) by Def4;
take  w ; ::_thesis: v + w = 0. (REAL-NS n)
thus v + w = v2 + (- v2) by Th2
.= 0. (REAL-NS n) by A9, RVSUM_1:22 ; ::_thesis: verum
end;
end;
hence  REAL-NS n is right_complementable ; ::_thesis: verum
end;
end;

theorem Th4: :: REAL_NS1:4
for n being Nat
for x being VECTOR of (REAL-NS n)
for a being Element of REAL n st x = a holds
- x = - a
proof
let n be Nat; ::_thesis: for x being VECTOR of (REAL-NS n)
for a being Element of REAL n st x = a holds
- x = - a
let x be VECTOR of (REAL-NS n); ::_thesis: for a being Element of REAL n st x = a holds
- x = - a
let a be Element of REAL n; ::_thesis: ( x = a implies - x = - a )
assume A1: x = a ; ::_thesis: - x = - a
reconsider a1 = a as Element of n -tuples_on REAL by EUCLID:def_1;
- x = (- 1) * x by RLVECT_1:16
.= - a1 by A1, Th3 ;
hence  - x = - a ; ::_thesis: verum
end;

theorem Th5: :: REAL_NS1:5
for n being Nat
for x, y being VECTOR of (REAL-NS n)
for a, b being Element of REAL n st x = a & y = b holds
x - y = a - b
proof
let n be Nat; ::_thesis: for x, y being VECTOR of (REAL-NS n)
for a, b being Element of REAL n st x = a & y = b holds
x - y = a - b
let x, y be VECTOR of (REAL-NS n); ::_thesis: for a, b being Element of REAL n st x = a & y = b holds
x - y = a - b
let a, b be Element of REAL n; ::_thesis: ( x = a & y = b implies x - y = a - b )
assume that
A1: x = a and
A2: y = b ; ::_thesis: x - y = a - b
 - y = - b by A2, Th4;
hence  x - y = a - b by A1, Th2; ::_thesis: verum
end;

theorem Th6: :: REAL_NS1:6
for n being Nat
for f being FinSequence of REAL st dom f = Seg n holds
f is Element of REAL n
proof
let n be Nat; ::_thesis: for f being FinSequence of REAL st dom f = Seg n holds
f is Element of REAL n
A1: n in NAT by ORDINAL1:def_12;
let f be FinSequence of REAL ; ::_thesis: ( dom f = Seg n implies f is Element of REAL n )
assume  dom f = Seg n ; ::_thesis: f is Element of REAL n
then  len f = n by A1, FINSEQ_1:def_3;
then  f is Element of n -tuples_on REAL by FINSEQ_2:92;
hence  f is Element of REAL n by EUCLID:def_1; ::_thesis: verum
end;

theorem Th7: :: REAL_NS1:7
for n being Nat
for x being Element of REAL n st ( for i being Element of NAT st i in Seg n holds
0 <= x . i ) holds
( 0 <= Sum x & ( for i being Element of NAT st i in Seg n holds
x . i <= Sum x ) )
proof
defpred S1[ Nat] means  for x being Element of REAL $1 st ( for i being Element of NAT st i in Seg $1 holds
0 <= x . i ) holds
( 0 <= Sum x & ( for i being Element of NAT st i in Seg $1 holds
x . i <= Sum x ) );
A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_x_being_Element_of_REAL_(k_+_1)_st_(_for_i_being_Element_of_NAT_st_i_in_Seg_(k_+_1)_holds_
0_<=_x_._i_)_holds_
(_0_<=_Sum_x_&_(_for_i_being_Element_of_NAT_st_i_in_Seg_(k_+_1)_holds_
x_._i_<=_Sum_x_)_)
let x be Element of REAL (k + 1); ::_thesis: ( ( for i being Element of NAT st i in Seg (k + 1) holds
0 <= x . i ) implies ( 0 <= Sum x & ( for i being Element of NAT st i in Seg (k + 1) holds
x . i <= Sum x ) ) )
assume A3: for i being Element of NAT st i in Seg (k + 1) holds
0 <= x . i ; ::_thesis: ( 0 <= Sum x & ( for i being Element of NAT st i in Seg (k + 1) holds
x . i <= Sum x ) )
thus  ( 0 <= Sum x & ( for i being Element of NAT st i in Seg (k + 1) holds
x . i <= Sum x ) ) ::_thesis: verum
proof
set xk = x | k;
A4: 0 <= x . (k + 1) by A3, FINSEQ_1:4;
A5: k + 1 = len x by CARD_1:def_7;
then  len (x | k) = k by FINSEQ_1:59, NAT_1:11;
then A6: x | k is Element of k -tuples_on REAL by FINSEQ_2:92;
 1 <= k + 1 by NAT_1:11;
then  k + 1 in Seg (len x) by A5, FINSEQ_1:1;
then A7: k + 1 in dom x by FINSEQ_1:def_3;
reconsider xk = x | k as Element of REAL k by A6, EUCLID:def_1;
A8: xk = x | (Seg k) by FINSEQ_1:def_15;
x = x | (k + 1) by A5, FINSEQ_1:58
.= x | (Seg (k + 1)) by FINSEQ_1:def_15
.= xk ^ <*(x . (k + 1))*> by A7, A8, FINSEQ_5:10 ;
then A9: Sum x = (Sum xk) + (x . (k + 1)) by RVSUM_1:74;
A10: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_k_holds_
0_<=_xk_._i
let i be Element of NAT ; ::_thesis: ( i in Seg k implies 0 <= xk . i )
assume A11: i in Seg k ; ::_thesis: 0 <= xk . i
 k <= k + 1 by NAT_1:11;
then  Seg k c= Seg (k + 1) by FINSEQ_1:5;
then  0 <= x . i by A3, A11;
then  0 <= (x | (Seg k)) . i by A11, FUNCT_1:49;
hence  0 <= xk . i by FINSEQ_1:def_15; ::_thesis: verum
end;
A12: k + 1 in Seg (k + 1) by FINSEQ_1:4;
A13: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_(k_+_1)_holds_
x_._i_<=_Sum_x
let i be Element of NAT ; ::_thesis: ( i in Seg (k + 1) implies x . b1 <= Sum x )
assume A14: i in Seg (k + 1) ; ::_thesis: x . b1 <= Sum x
then A15: 1 <= i by FINSEQ_1:1;
A16: i <= k + 1 by A14, FINSEQ_1:1;
percases ( i < k + 1 or i = k + 1 ) by A16, XXREAL_0:1;
suppose i < k + 1 ; ::_thesis: x . b1 <= Sum x
then  i <= k by NAT_1:13;
then A17: i in Seg k by A15, FINSEQ_1:1;
then  xk . i <= Sum xk by A2, A10;
then A18: x . i <= Sum xk by A8, A17, FUNCT_1:49;
 Sum xk <= (Sum xk) + (x . (k + 1)) by A3, A12, XREAL_1:31;
hence  x . i <= Sum x by A9, A18, XXREAL_0:2; ::_thesis: verum
end;
suppose i = k + 1 ; ::_thesis: x . b1 <= Sum x
hence  x . i <= Sum x by A2, A10, A9, XREAL_1:31; ::_thesis: verum
end;
end;
end;
 0 <= Sum xk by A2, A10;
hence  ( 0 <= Sum x & ( for i being Element of NAT st i in Seg (k + 1) holds
x . i <= Sum x ) ) by A4, A9, A13; ::_thesis: verum
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A19: S1[ 0 ] by RVSUM_1:72;
thus  for k being Nat holds S1[k] from NAT_1:sch_2(A19, A1); ::_thesis: verum
end;

theorem Th8: :: REAL_NS1:8
for n being Nat
for x being Element of REAL n
for i being Nat st i in Seg n holds
abs (x . i) <= |.x.|
proof
let n be Nat; ::_thesis: for x being Element of REAL n
for i being Nat st i in Seg n holds
abs (x . i) <= |.x.|
let x be Element of REAL n; ::_thesis: for i being Nat st i in Seg n holds
abs (x . i) <= |.x.|
let i be Nat; ::_thesis: ( i in Seg n implies abs (x . i) <= |.x.| )
reconsider sx = sqr x as Element of REAL n by EUCLID:def_1;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_Seg_n_holds_
0_<=_sx_._k
let k be Element of NAT ; ::_thesis: ( k in Seg n implies 0 <= sx . k )
assume  k in Seg n ; ::_thesis: 0 <= sx . k
 sx . k = (x . k) ^2 by VALUED_1:11;
hence  0 <= sx . k by XREAL_1:63; ::_thesis: verum
end;
A2: 0 <= (abs (x . i)) * (abs (x . i)) by XREAL_1:63;
 (abs (x . i)) * (abs (x . i)) = (x . i) ^2
proof
percases ( abs (x . i) = x . i or abs (x . i) = - (x . i) ) by ABSVALUE:1;
suppose abs (x . i) = x . i ; ::_thesis: (abs (x . i)) * (abs (x . i)) = (x . i) ^2
hence  (abs (x . i)) * (abs (x . i)) = (x . i) ^2 ; ::_thesis: verum
end;
suppose abs (x . i) = - (x . i) ; ::_thesis: (abs (x . i)) * (abs (x . i)) = (x . i) ^2
hence  (abs (x . i)) * (abs (x . i)) = (x . i) ^2 ; ::_thesis: verum
end;
end;
end;
then A3: (sqr x) . i = (abs (x . i)) * (abs (x . i)) by VALUED_1:11;
assume  i in Seg n ; ::_thesis: abs (x . i) <= |.x.|
then  (abs (x . i)) * (abs (x . i)) <= Sum (sqr x) by A3, A1, Th7;
then A4: sqrt ((abs (x . i)) * (abs (x . i))) <= sqrt (Sum (sqr x)) by A2, SQUARE_1:26;
 sqrt ((abs (x . i)) ^2) = abs (x . i) by COMPLEX1:46, SQUARE_1:22;
hence  abs (x . i) <= |.x.| by A4, EUCLID:def_5; ::_thesis: verum
end;

theorem Th9: :: REAL_NS1:9
for n being Nat
for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
for i being Nat st i in Seg n holds
abs (y . i) <= ||.x.||
proof
let n be Nat; ::_thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
for i being Nat st i in Seg n holds
abs (y . i) <= ||.x.||
let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st x = y holds
for i being Nat st i in Seg n holds
abs (y . i) <= ||.x.||
let y be Element of REAL n; ::_thesis: ( x = y implies for i being Nat st i in Seg n holds
abs (y . i) <= ||.x.|| )
assume  x = y ; ::_thesis: for i being Nat st i in Seg n holds
abs (y . i) <= ||.x.||
then  ||.x.|| = |.y.| by Th1;
hence  for i being Nat st i in Seg n holds
abs (y . i) <= ||.x.|| by Th8; ::_thesis: verum
end;

theorem Th10: :: REAL_NS1:10
for n being Nat
for x being Element of REAL (n + 1) holds |.x.| ^2 = (|.(x | n).| ^2) + ((x . (n + 1)) ^2)
proof
let n be Nat; ::_thesis: for x being Element of REAL (n + 1) holds |.x.| ^2 = (|.(x | n).| ^2) + ((x . (n + 1)) ^2)
let x be Element of REAL (n + 1); ::_thesis: |.x.| ^2 = (|.(x | n).| ^2) + ((x . (n + 1)) ^2)
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider x = x as Element of (n + 1) -tuples_on REAL by EUCLID:def_1;
A1: x | n = x | (Seg n) by FINSEQ_1:def_15;
A2: n + 1 = len x by CARD_1:def_7;
then  n + 1 in Seg (len x) by FINSEQ_1:4;
then A3: n + 1 in dom x by FINSEQ_1:def_3;
 len (x | n) = n by A2, FINSEQ_1:59, NAT_1:11;
then reconsider xn = x | n as Element of n -tuples_on REAL by FINSEQ_2:92;
 ( sqr x is Element of REAL (n + 1) & ( for k being Element of NAT st k in Seg (n + 1) holds
0 <= (sqr x) . k ) )
proof
thus  sqr x is Element of REAL (n + 1) by EUCLID:def_1; ::_thesis: for k being Element of NAT st k in Seg (n + 1) holds
0 <= (sqr x) . k
let k be Element of NAT ; ::_thesis: ( k in Seg (n + 1) implies 0 <= (sqr x) . k )
assume  k in Seg (n + 1) ; ::_thesis: 0 <= (sqr x) . k
(sqr x) . k = (x . k) ^2 by VALUED_1:11
.= (x . k) * (x . k) ;
hence  0 <= (sqr x) . k by XREAL_1:63; ::_thesis: verum
end;
then  ( |.x.| = sqrt (Sum (sqr x)) & 0 <= Sum (sqr x) ) by Th7, EUCLID:def_5;
then A4: |.x.| ^2 = Sum (sqr x) by SQUARE_1:def_2;
 ( sqr (x | n) is Element of REAL n & ( for k being Element of NAT st k in Seg n holds
0 <= (sqr (x | n)) . k ) )
proof
 sqr xn is Element of REAL n by EUCLID:def_1;
hence  sqr (x | n) is Element of REAL n ; ::_thesis: for k being Element of NAT st k in Seg n holds
0 <= (sqr (x | n)) . k
let k be Element of NAT ; ::_thesis: ( k in Seg n implies 0 <= (sqr (x | n)) . k )
assume  k in Seg n ; ::_thesis: 0 <= (sqr (x | n)) . k
(sqr xn) . k = (xn . k) ^2 by VALUED_1:11
.= (xn . k) * (xn . k) ;
hence  0 <= (sqr (x | n)) . k by XREAL_1:63; ::_thesis: verum
end;
then  ( |.(x | n).| = sqrt (Sum (sqr (x | n))) & 0 <= Sum (sqr (x | n)) ) by Th7, EUCLID:def_5;
then A5: (|.(x | n).| ^2) + ((x . (n + 1)) ^2) = (Sum (sqr (x | n))) + ((x . (n + 1)) ^2) by SQUARE_1:def_2;
A6: x = x | (n + 1) by A2, FINSEQ_1:58
.= x | (Seg (n + 1)) by FINSEQ_1:def_15
.= (x | n) ^ <*(x . (n + 1))*> by A3, A1, FINSEQ_5:10 ;
(sqr (x | n)) ^ <*((x . (n + 1)) ^2)*> = (mlt (xn,xn)) ^ <*((x . (n + 1)) * (x . (n + 1)))*>
.= mlt ((xn ^ <*(x . (n + 1))*>),((x | n) ^ <*(x . (n + 1))*>)) by RFUNCT_4:2
.= sqr x by A6 ;
hence  |.x.| ^2 = (|.(x | n).| ^2) + ((x . (n + 1)) ^2) by A4, A5, RVSUM_1:74; ::_thesis: verum
end;

definition
let n be Nat;
let f be Function of NAT,(REAL n);
let k be Nat;
:: original: .
redefine funcf . k ->  Element of REAL n;
coherence
 f . k is Element of REAL n
proof
 f . k in REAL n ;
hence  f . k is Element of REAL n ; ::_thesis: verum
end;
end;

theorem Th11: :: REAL_NS1:11
for n being Nat
for x being Point of (REAL-NS n)
for xs being Element of REAL n
for seq being sequence of (REAL-NS n)
for xseq being Function of NAT,(REAL n) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg n holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
proof
defpred S1[ Nat] means  for x being Point of (REAL-NS $1)
for xs being Element of REAL $1
for seq being sequence of (REAL-NS $1)
for xseq being Function of NAT,(REAL $1) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg $1 holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) );
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_x_being_Point_of_(REAL-NS_(n_+_1))
for_xs_being_Element_of_REAL_(n_+_1)
for_seq_being_sequence_of_(REAL-NS_(n_+_1))
for_xseq_being_Function_of_NAT,(REAL_(n_+_1))_st_xs_=_x_&_xseq_=_seq_holds_
(_(_seq_is_convergent_&_lim_seq_=_x_)_iff_for_i_being_Element_of_NAT_st_i_in_Seg_(n_+_1)_holds_
ex_rseqi_being_Real_Sequence_st_
for_k_being_Element_of_NAT_holds_
(_rseqi_._k_=_(xseq_._k)_._i_&_rseqi_is_convergent_&_xs_._i_=_lim_rseqi_)_)
let x be Point of (REAL-NS (n + 1)); ::_thesis: for xs being Element of REAL (n + 1)
for seq being sequence of (REAL-NS (n + 1))
for xseq being Function of NAT,(REAL (n + 1)) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
let xs be Element of REAL (n + 1); ::_thesis: for seq being sequence of (REAL-NS (n + 1))
for xseq being Function of NAT,(REAL (n + 1)) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
let seq be sequence of (REAL-NS (n + 1)); ::_thesis: for xseq being Function of NAT,(REAL (n + 1)) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
let xseq be Function of NAT,(REAL (n + 1)); ::_thesis: ( xs = x & xseq = seq implies ( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) )
assume A3: ( xs = x & xseq = seq ) ; ::_thesis: ( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
A4: now__::_thesis:_(_(_for_i_being_Element_of_NAT_st_i_in_Seg_(n_+_1)_holds_
ex_rseqi_being_Real_Sequence_st_
for_k_being_Element_of_NAT_holds_
(_rseqi_._k_=_(xseq_._k)_._i_&_rseqi_is_convergent_&_xs_._i_=_lim_rseqi_)_)_implies_(_seq_is_convergent_&_lim_seq_=_x_)_)
assume A5: for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; ::_thesis: ( seq is convergent & lim seq = x )
thus  ( seq is convergent & lim seq = x ) ::_thesis: verum
proof
 len xs = n + 1 by CARD_1:def_7;
then  len (xs | n) = n by FINSEQ_1:59, NAT_1:11;
then  dom (xs | n) = Seg n by FINSEQ_1:def_3;
then reconsider xsn = xs | n as Element of REAL n by Th6;
reconsider xn = xsn as Point of (REAL-NS n) by Def4;
defpred S2[ Element of NAT , Element of REAL n] means $2 = (xseq . $1) | n;
set seq2 = ||.(seq - x).|| (#) ||.(seq - x).||;
consider rseqn1 being Real_Sequence such that
A6: for k being Element of NAT holds
( rseqn1 . k = (xseq . k) . (n + 1) & rseqn1 is convergent & xs . (n + 1) = lim rseqn1 ) by A5, FINSEQ_1:4;
A7: for i being Element of NAT ex y being Element of REAL n st S2[i,y]
proof
let i be Element of NAT ; ::_thesis: ex y being Element of REAL n st S2[i,y]
take y = (xseq . i) | n; ::_thesis: ( y is Element of REAL n & S2[i,y] )
 len (xseq . i) = n + 1 by CARD_1:def_7;
then  len ((xseq . i) | n) = n by FINSEQ_1:59, NAT_1:11;
then  dom ((xseq . i) | n) = Seg n by FINSEQ_1:def_3;
hence  ( y is Element of REAL n & S2[i,y] ) by Th6; ::_thesis: verum
end;
consider xseqn being Function of NAT,(REAL n) such that
A8: for i being Element of NAT holds S2[i,xseqn . i] from FUNCT_2:sch_3(A7);
reconsider seqn = xseqn as sequence of (REAL-NS n) by Def4;
set seqn2 = ||.(seqn - xn).|| (#) ||.(seqn - xn).||;
deffunc H1( Element of NAT ) ->  Element of REAL = abs ((rseqn1 . $1) - (xs . (n + 1)));
consider absrseq being Real_Sequence such that
A9: for i being Element of NAT holds absrseq . i = H1(i) from SEQ_1:sch_1();
A10: for i being Element of NAT st i in Seg n holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi ) )
assume A11: i in Seg n ; ::_thesis: ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi )
 n <= n + 1 by NAT_1:11;
then  Seg n c= Seg (n + 1) by FINSEQ_1:5;
then consider rseqi being Real_Sequence such that
A12: for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A5, A11;
A13: now__::_thesis:_for_k_being_Element_of_NAT_holds_rseqi_._k_=_(xseqn_._k)_._i
let k be Element of NAT ; ::_thesis: rseqi . k = (xseqn . k) . i
thus rseqi . k = (xseq . k) . i by A12
.= ((xseq . k) | (Seg n)) . i by A11, FUNCT_1:49
.= ((xseq . k) | n) . i by FINSEQ_1:def_15
.= (xseqn . k) . i by A8 ; ::_thesis: verum
end;
xsn . i = (xs | (Seg n)) . i by FINSEQ_1:def_15
.= xs . i by A11, FUNCT_1:49 ;
hence  ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseqn . k) . i & rseqi is convergent & xsn . i = lim rseqi ) by A12, A13; ::_thesis: verum
end;
then A14: xn = lim seqn by A2;
set rseqn2 = absrseq (#) absrseq;
 xsn = xn ;
then A15: seqn is convergent by A2, A10;
then A16: ||.(seqn - xn).|| is convergent by A14, NORMSP_1:24;
then A17: ||.(seqn - xn).|| (#) ||.(seqn - xn).|| is convergent by SEQ_2:14;
now__::_thesis:_for_k_being_Element_of_NAT_holds_(||.(seq_-_x).||_(#)_||.(seq_-_x).||)_._k_=_((||.(seqn_-_xn).||_(#)_||.(seqn_-_xn).||)_._k)_+_((absrseq_(#)_absrseq)_._k)
reconsider rxs = xs as Element of (n + 1) -tuples_on REAL by EUCLID:def_1;
let k be Element of NAT ; ::_thesis: (||.(seq - x).|| (#) ||.(seq - x).||) . k = ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k)
A18: ||.(seq - x).|| . k = ||.((seq - x) . k).|| by NORMSP_0:def_4
.= ||.((seq . k) - x).|| by NORMSP_1:def_4 ;
reconsider rxseqk = xseq . k as Element of (n + 1) -tuples_on REAL by EUCLID:def_1;
A19: ||.(seqn - xn).|| . k = ||.((seqn - xn) . k).|| by NORMSP_0:def_4
.= ||.((seqn . k) - xn).|| by NORMSP_1:def_4 ;
 len ((xseqn . k) - xsn) = n by CARD_1:def_7;
then A20: dom ((xseqn . k) - xsn) = Seg n by FINSEQ_1:def_3;
A21: ((xseq . k) - xs) . (n + 1) = (rxseqk . (n + 1)) - (rxs . (n + 1)) by RVSUM_1:27
.= (rseqn1 . k) - (xs . (n + 1)) by A6 ;
 len ((xseq . k) - xs) = n + 1 by CARD_1:def_7;
then A22: len (((xseq . k) - xs) | n) = n by FINSEQ_1:59, NAT_1:11;
A23: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(((xseq_._k)_-_xs)_|_n)_holds_
(((xseq_._k)_-_xs)_|_n)_._i_=_((xseqn_._k)_-_xsn)_._i
reconsider xseq2 = xseqn . k, xs2 = xsn as Element of n -tuples_on REAL by EUCLID:def_1;
reconsider xseq1 = xseq . k, xs1 = xs as Element of (n + 1) -tuples_on REAL by EUCLID:def_1;
let i be Nat; ::_thesis: ( i in dom (((xseq . k) - xs) | n) implies (((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . i )
assume  i in dom (((xseq . k) - xs) | n) ; ::_thesis: (((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . i
then A24: i in Seg n by A22, FINSEQ_1:def_3;
A25: ((xseqn . k) - xsn) . i = (xseq2 . i) - (xs2 . i) by RVSUM_1:27;
A26: ((xseq . k) - xs) . i = (xseq1 . i) - (xs1 . i) by RVSUM_1:27;
thus (((xseq . k) - xs) | n) . i = (((xseq . k) - xs) | (Seg n)) . i by FINSEQ_1:def_15
.= ((xseq . k) - xs) . i by A24, FUNCT_1:49
.= (((xseq . k) | (Seg n)) . i) - (xs . i) by A24, A26, FUNCT_1:49
.= (((xseq . k) | (Seg n)) . i) - ((xs | (Seg n)) . i) by A24, FUNCT_1:49
.= (((xseq . k) | n) . i) - ((xs | (Seg n)) . i) by FINSEQ_1:def_15
.= (((xseq . k) | n) . i) - ((xs | n) . i) by FINSEQ_1:def_15
.= ((xseqn . k) - xsn) . i by A8, A25 ; ::_thesis: verum
end;
 dom (((xseq . k) - xs) | n) = Seg n by A22, FINSEQ_1:def_3;
then A27: ((xseq . k) - xs) | n = (xseqn . k) - xsn by A20, A23, FINSEQ_1:13;
A28: 0 <= ((rseqn1 . k) - (xs . (n + 1))) ^2 by XREAL_1:63;
A29: absrseq . k = abs ((rseqn1 . k) - (xs . (n + 1))) by A9;
 ||.((seq . k) - x).|| = |.((xseq . k) - xs).| by A3, Th1, Th5;
hence (||.(seq - x).|| (#) ||.(seq - x).||) . k = |.((xseq . k) - xs).| ^2 by A18, SEQ_1:8
.= (|.((xseqn . k) - xsn).| ^2) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by A21, A27, Th10
.= (||.((seqn . k) - xn).|| ^2) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by Th1, Th5
.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (((rseqn1 . k) - (xs . (n + 1))) ^2) by A19, SEQ_1:8
.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (abs (((rseqn1 . k) - (xs . (n + 1))) * ((rseqn1 . k) - (xs . (n + 1))))) by A28, ABSVALUE:def_1
.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((abs ((rseqn1 . k) - (xs . (n + 1)))) * (abs ((rseqn1 . k) - (xs . (n + 1))))) by COMPLEX1:65
.= ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k) by A29, SEQ_1:8 ;
::_thesis: verum
end;
then A30: ||.(seq - x).|| (#) ||.(seq - x).|| = (||.(seqn - xn).|| (#) ||.(seqn - xn).||) + (absrseq (#) absrseq) by SEQ_1:7;
A31: now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_m_being_Element_of_NAT_st_
for_k_being_Element_of_NAT_st_m_<=_k_holds_
abs_((absrseq_._k)_-_0)_<_e
let e be real number ; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for k being Element of NAT st m <= k holds
abs ((absrseq . k) - 0) < e )
assume  e > 0 ; ::_thesis: ex m being Element of NAT st
for k being Element of NAT st m <= k holds
abs ((absrseq . k) - 0) < e
then consider m being Element of NAT  such that
A32: for k being Element of NAT st m <= k holds
abs ((rseqn1 . k) - (xs . (n + 1))) < e by A6, SEQ_2:def_7;
now__::_thesis:_for_k_being_Element_of_NAT_st_m_<=_k_holds_
abs_((absrseq_._k)_-_0)_<_e
let k be Element of NAT ; ::_thesis: ( m <= k implies abs ((absrseq . k) - 0) < e )
assume  m <= k ; ::_thesis: abs ((absrseq . k) - 0) < e
then  abs ((abs ((rseqn1 . k) - (xs . (n + 1)))) - 0) < e by A32;
hence  abs ((absrseq . k) - 0) < e by A9; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for k being Element of NAT st m <= k holds
abs ((absrseq . k) - 0) < e ; ::_thesis: verum
end;
then A33: absrseq is convergent by SEQ_2:def_6;
then  lim absrseq = 0 by A31, SEQ_2:def_7;
then A34: lim (absrseq (#) absrseq) = 0 * 0 by A33, SEQ_2:15
.= 0 ;
A35: absrseq (#) absrseq is convergent by A33, SEQ_2:14;
then A36: ||.(seq - x).|| (#) ||.(seq - x).|| is convergent by A17, A30, SEQ_2:5;
 lim ||.(seqn - xn).|| = 0 by A15, A14, NORMSP_1:24;
then  lim (||.(seqn - xn).|| (#) ||.(seqn - xn).||) = 0 * 0 by A16, SEQ_2:15
.= 0 ;
then A37: lim (||.(seq - x).|| (#) ||.(seq - x).||) = 0 + 0 by A17, A35, A34, A30, SEQ_2:6
.= 0 ;
A38: for e being Real st e > 0 holds
ex m being Element of NAT st
for k being Element of NAT st k >= m holds
||.((seq . k) - x).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for k being Element of NAT st k >= m holds
||.((seq . k) - x).|| < e )
assume A39: e > 0 ; ::_thesis: ex m being Element of NAT st
for k being Element of NAT st k >= m holds
||.((seq . k) - x).|| < e
 e * 0 < e * e by A39, XREAL_1:97;
then consider m being Element of NAT  such that
A40: for k being Element of NAT st m <= k holds
abs (((||.(seq - x).|| (#) ||.(seq - x).||) . k) - 0) < e * e by A36, A37, SEQ_2:def_7;
now__::_thesis:_for_k_being_Element_of_NAT_st_m_<=_k_holds_
||.((seq_._k)_-_x).||_<_e
let k be Element of NAT ; ::_thesis: ( m <= k implies ||.((seq . k) - x).|| < e )
assume A41: m <= k ; ::_thesis: ||.((seq . k) - x).|| < e
||.(seq - x).|| . k = ||.((seq - x) . k).|| by NORMSP_0:def_4
.= ||.((seq . k) - x).|| by NORMSP_1:def_4 ;
then  (||.(seq - x).|| (#) ||.(seq - x).||) . k = ||.((seq . k) - x).|| * ||.((seq . k) - x).|| by SEQ_1:8;
then  abs (((||.(seq - x).|| (#) ||.(seq - x).||) . k) - 0) = ||.((seq . k) - x).|| * ||.((seq . k) - x).|| by ABSVALUE:def_1;
then A42: ||.((seq . k) - x).|| * ||.((seq . k) - x).|| < e * e by A40, A41;
A43: sqrt (||.((seq . k) - x).|| * ||.((seq . k) - x).||) = sqrt (||.((seq . k) - x).|| ^2)
.= ||.((seq . k) - x).|| by SQUARE_1:22 ;
sqrt (e * e) = sqrt (e ^2)
.= e by A39, SQUARE_1:22 ;
hence  ||.((seq . k) - x).|| < e by A42, A43, SQUARE_1:27; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for k being Element of NAT st k >= m holds
||.((seq . k) - x).|| < e ; ::_thesis: verum
end;
then  seq is convergent by NORMSP_1:def_6;
hence  ( seq is convergent & lim seq = x ) by A38, NORMSP_1:def_7; ::_thesis: verum
end;
end;
now__::_thesis:_(_seq_is_convergent_&_lim_seq_=_x_implies_for_i_being_Element_of_NAT_st_i_in_Seg_(n_+_1)_holds_
ex_rseqi_being_Real_Sequence_st_
for_k_being_Element_of_NAT_holds_
(_rseqi_._k_=_(xseq_._k)_._i_&_rseqi_is_convergent_&_xs_._i_=_lim_rseqi_)_)
assume A44: ( seq is convergent & lim seq = x ) ; ::_thesis: for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi )
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_(n_+_1)_holds_
ex_rseqi_being_Real_Sequence_st_
for_k_being_Element_of_NAT_holds_
(_rseqi_._k_=_(xseq_._k)_._i_&_rseqi_is_convergent_&_xs_._i_=_lim_rseqi_)
let i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) implies ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
assume A45: i in Seg (n + 1) ; ::_thesis: ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi )
deffunc H1( Element of NAT ) ->  Element of REAL = (xseq . $1) . i;
consider rseqi being Real_Sequence such that
A46: for l being Element of NAT holds rseqi . l = H1(l) from SEQ_1:sch_1();
A47: now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((rseqi_._m)_-_(xs_._i))_<_e
let e be real number ; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (xs . i)) < e )
assume A48: e > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (xs . i)) < e
thus  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (xs . i)) < e ::_thesis: verum
proof
 e is Real by XREAL_0:def_1;
then consider k being Element of NAT  such that
A49: for m being Element of NAT st m >= k holds
||.((seq . m) - x).|| < e by A44, A48, NORMSP_1:def_7;
take  k ; ::_thesis: for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (xs . i)) < e
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((rseqi . m) - (xs . i)) < e )
assume  k <= m ; ::_thesis: abs ((rseqi . m) - (xs . i)) < e
then A50: ||.((seq . m) - x).|| < e by A49;
 len ((xseq . m) - xs) = n + 1 by CARD_1:def_7;
then  i in dom ((xseq . m) - xs) by A45, FINSEQ_1:def_3;
then  ((xseq . m) . i) - (xs . i) = ((xseq . m) - xs) . i by VALUED_1:13;
then A51: abs (((xseq . m) . i) - (xs . i)) <= ||.((seq . m) - x).|| by A3, A45, Th5, Th9;
 (rseqi . m) - (xs . i) = ((xseq . m) . i) - (xs . i) by A46;
hence  abs ((rseqi . m) - (xs . i)) < e by A50, A51, XXREAL_0:2; ::_thesis: verum
end;
end;
then A52: rseqi is convergent by SEQ_2:def_6;
then  xs . i = lim rseqi by A47, SEQ_2:def_7;
hence  ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A46, A52; ::_thesis: verum
end;
hence  for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; ::_thesis: verum
end;
hence  ( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) by A4; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
A53: S1[ 0 ]
proof
let x be Point of (REAL-NS 0); ::_thesis: for xs being Element of REAL 0
for seq being sequence of (REAL-NS 0)
for xseq being Function of NAT,(REAL 0) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg 0 holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
let xs be Element of REAL 0; ::_thesis: for seq being sequence of (REAL-NS 0)
for xseq being Function of NAT,(REAL 0) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg 0 holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
let seq be sequence of (REAL-NS 0); ::_thesis: for xseq being Function of NAT,(REAL 0) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg 0 holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
let xseq be Function of NAT,(REAL 0); ::_thesis: ( xs = x & xseq = seq implies ( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg 0 holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) )
assume that
A54: xs = x and
A55: xseq = seq ; ::_thesis: ( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg 0 holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )
now__::_thesis:_(_(_for_i_being_Element_of_NAT_st_i_in_Seg_0_holds_
ex_rseqi_being_Real_Sequence_st_
for_k_being_Element_of_NAT_holds_
(_rseqi_._k_=_(xseq_._k)_._i_&_rseqi_is_convergent_&_xs_._i_=_lim_rseqi_)_)_implies_(_seq_is_convergent_&_lim_seq_=_x_)_)
assume  for i being Element of NAT st i in Seg 0 holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ; ::_thesis: ( seq is convergent & lim seq = x )
A56: for i being Element of NAT holds seq . i = 0. (REAL-NS 0)
proof
let i be Element of NAT ; ::_thesis: seq . i = 0. (REAL-NS 0)
 xseq . i = 0.REAL 0 ;
hence  seq . i = 0. (REAL-NS 0) by A55, Def4; ::_thesis: verum
end;
 xs = 0* 0 ;
then A57: x = 0. (REAL-NS 0) by A54, Def4;
A58: for r being Real st 0 < r holds
ex m being Element of NAT st
for k being Element of NAT st m <= k holds
||.((seq . k) - x).|| < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for k being Element of NAT st m <= k holds
||.((seq . k) - x).|| < r )
assume A59: 0 < r ; ::_thesis: ex m being Element of NAT st
for k being Element of NAT st m <= k holds
||.((seq . k) - x).|| < r
take m = 1; ::_thesis: for k being Element of NAT st m <= k holds
||.((seq . k) - x).|| < r
let k be Element of NAT ; ::_thesis: ( m <= k implies ||.((seq . k) - x).|| < r )
assume  m <= k ; ::_thesis: ||.((seq . k) - x).|| < r
||.((seq . k) - x).|| = ||.((0. (REAL-NS 0)) - (0. (REAL-NS 0))).|| by A57, A56
.= ||.(0. (REAL-NS 0)).|| by RLVECT_1:15
.= 0 ;
hence  ||.((seq . k) - x).|| < r by A59; ::_thesis: verum
end;
then  seq is convergent by NORMSP_1:def_6;
hence  ( seq is convergent & lim seq = x ) by A58, NORMSP_1:def_7; ::_thesis: verum
end;
hence  ( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg 0 holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) ; ::_thesis: verum
end;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A53, A1); ::_thesis: verum
end;

theorem Th12: :: REAL_NS1:12
for n being Nat
for f being sequence of (REAL-NS n) st f is Cauchy_sequence_by_Norm holds
f is convergent
proof
let n be Nat; ::_thesis: for f being sequence of (REAL-NS n) st f is Cauchy_sequence_by_Norm holds
f is convergent
let vseq be sequence of (REAL-NS n); ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
reconsider xvseq = vseq as Function of NAT,(REAL n) by Def4;
defpred S1[ set , set ] means  ex rseqi being Real_Sequence st
for l being Element of NAT holds
( rseqi . l = (xvseq . l) . $1 & rseqi is convergent & $2 = lim rseqi );
A2: for i being Nat st i in Seg n holds
ex y being Element of REAL st S1[i,y]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex y being Element of REAL st S1[i,y] )
assume A3: i in Seg n ; ::_thesis: ex y being Element of REAL st S1[i,y]
deffunc H1( Element of NAT ) ->  Element of REAL = (xvseq . $1) . i;
consider rseqi being Real_Sequence such that
A4: for l being Element of NAT holds rseqi . l = H1(l) from SEQ_1:sch_1();
take  lim rseqi ; ::_thesis: S1[i, lim rseqi]
now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((rseqi_._m)_-_(rseqi_._k))_<_e
let e be real number ; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e )
assume A5: e > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
thus  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e ::_thesis: verum
proof
 e is Real by XREAL_0:def_1;
then consider k being Element of NAT  such that
A6: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A5, RSSPACE3:8;
take  k ; ::_thesis: for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume  k <= m ; ::_thesis: abs ((rseqi . m) - (rseqi . k)) < e
then A7: ||.((vseq . m) - (vseq . k)).|| < e by A6;
 len ((xvseq . m) - (xvseq . k)) = n by CARD_1:def_7;
then  i in dom ((xvseq . m) - (xvseq . k)) by A3, FINSEQ_1:def_3;
then  ((xvseq . m) . i) - ((xvseq . k) . i) = ((xvseq . m) - (xvseq . k)) . i by VALUED_1:13;
then A8: abs (((xvseq . m) . i) - ((xvseq . k) . i)) <= ||.((vseq . m) - (vseq . k)).|| by A3, Th5, Th9;
 ( rseqi . m = (xvseq . m) . i & rseqi . k = (xvseq . k) . i ) by A4;
hence  abs ((rseqi . m) - (rseqi . k)) < e by A7, A8, XXREAL_0:2; ::_thesis: verum
end;
end;
then  rseqi is convergent by SEQ_4:41;
hence  S1[i, lim rseqi] by A4; ::_thesis: verum
end;
consider f being FinSequence of REAL  such that
A9: ( dom f = Seg n & ( for k being Nat st k in Seg n holds
S1[k,f . k] ) ) from FINSEQ_1:sch_5(A2);
reconsider tseq = f as Element of REAL n by A9, Th6;
reconsider xseq = tseq as Point of (REAL-NS n) by Def4;
A10: xseq = tseq ;
 for k being Element of NAT st k in Seg n holds
S1[k,f . k] by A9;
hence  vseq is convergent by A10, Th11; ::_thesis: verum
end;

Lm2:  for n being Nat holds REAL-NS n is RealBanachSpace
proof
let n be Nat; ::_thesis: REAL-NS n is RealBanachSpace
 for seq being sequence of (REAL-NS n) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th12;
hence  REAL-NS n is RealBanachSpace by LOPBAN_1:def_15; ::_thesis: verum
end;

registration
let n be Nat;
cluster REAL-NS n ->  non empty strict complete ;
coherence
 REAL-NS n is complete by Lm2;
end;

begin

definition
let n be Nat;
func Euclid_scalar n ->  Function of [:(REAL n),(REAL n):],REAL means :Def5: :: REAL_NS1:def 5
 for x, y being Element of REAL n holds it . (x,y) = Sum (mlt (x,y));
existence
 ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y))
proof
deffunc H1( Element of REAL n, Element of REAL n) ->  Element of REAL = Sum (mlt ($1,$2));
 ex f being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
hence  ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y)) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y)) ) & ( for x, y being Element of REAL n holds b2 . (x,y) = Sum (mlt (x,y)) ) holds
b1 = b2
proof
let scalar1, scalar2 be Function of [:(REAL n),(REAL n):],REAL; ::_thesis: ( ( for x, y being Element of REAL n holds scalar1 . (x,y) = Sum (mlt (x,y)) ) & ( for x, y being Element of REAL n holds scalar2 . (x,y) = Sum (mlt (x,y)) ) implies scalar1 = scalar2 )
assume that
A1: for x, y being Element of REAL n holds scalar1 . (x,y) = Sum (mlt (x,y)) and
A2: for x, y being Element of REAL n holds scalar2 . (x,y) = Sum (mlt (x,y)) ; ::_thesis: scalar1 = scalar2
 for x, y being Element of REAL n holds scalar1 . (x,y) = scalar2 . (x,y)
proof
let x, y be Element of REAL n; ::_thesis: scalar1 . (x,y) = scalar2 . (x,y)
 scalar1 . (x,y) = Sum (mlt (x,y)) by A1;
hence  scalar1 . (x,y) = scalar2 . (x,y) by A2; ::_thesis: verum
end;
hence  scalar1 = scalar2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Euclid_scalar REAL_NS1:def_5_:_
 for n being Nat
for b2 being Function of [:(REAL n),(REAL n):],REAL holds
( b2 = Euclid_scalar n iff for x, y being Element of REAL n holds b2 . (x,y) = Sum (mlt (x,y)) );

definition
let n be Nat;
func REAL-US n ->  non empty strict UNITSTR  means :Def6: :: REAL_NS1:def 6
( the carrier of it = REAL n & 0. it = 0* n & the addF of it = Euclid_add n & the Mult of it = Euclid_mult n & the scalar of it = Euclid_scalar n );
existence
 ex b1 being non empty strict UNITSTR st
( the carrier of b1 = REAL n & 0. b1 = 0* n & the addF of b1 = Euclid_add n & the Mult of b1 = Euclid_mult n & the scalar of b1 = Euclid_scalar n )
proof
take  UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) ; ::_thesis: ( the carrier of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = REAL n & 0. UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = 0* n & the addF of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_add n & the Mult of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_mult n & the scalar of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_scalar n )
thus  ( the carrier of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = REAL n & 0. UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = 0* n & the addF of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_add n & the Mult of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_mult n & the scalar of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_scalar n ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict UNITSTR st the carrier of b1 = REAL n & 0. b1 = 0* n & the addF of b1 = Euclid_add n & the Mult of b1 = Euclid_mult n & the scalar of b1 = Euclid_scalar n & the carrier of b2 = REAL n & 0. b2 = 0* n & the addF of b2 = Euclid_add n & the Mult of b2 = Euclid_mult n & the scalar of b2 = Euclid_scalar n holds
b1 = b2 ;
end;

:: deftheorem Def6 defines REAL-US REAL_NS1:def_6_:_
 for n being Nat
for b2 being non empty strict UNITSTR holds
( b2 = REAL-US n iff ( the carrier of b2 = REAL n & 0. b2 = 0* n & the addF of b2 = Euclid_add n & the Mult of b2 = Euclid_mult n & the scalar of b2 = Euclid_scalar n ) );

registration
let n be non empty Nat;
cluster REAL-US n ->  non empty non trivial strict ;
coherence
 not REAL-US n is trivial
proof
the carrier of (REAL-US n) = REAL n by Def6
.= the carrier of (TOP-REAL n) by EUCLID:22 ;
hence  not REAL-US n is trivial ; ::_thesis: verum
end;
end;

registration
let n be Nat;
cluster REAL-US n ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ;
coherence
 ( REAL-US n is RealUnitarySpace-like & REAL-US n is vector-distributive & REAL-US n is scalar-distributive & REAL-US n is scalar-associative & REAL-US n is scalar-unital & REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
proof
A1: n in NAT by ORDINAL1:def_12;
now__::_thesis:_for_x,_y,_z_being_Point_of_(REAL-US_n)
for_a_being_Real_holds_
(_0_<=_x_.|._x_&_(_x_.|._x_=_0_implies_x_=_0._(REAL-US_n)_)_&_(_x_=_0._(REAL-US_n)_implies_x_.|._x_=_0_)_&_x_.|._y_=_y_.|._x_&_(x_+_y)_.|._z_=_(x_.|._z)_+_(y_.|._z)_&_(a_*_x)_.|._y_=_a_*_(x_.|._y)_)
let x, y, z be Point of (REAL-US n); ::_thesis: for a being Real holds
( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let a be Real; ::_thesis: ( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
reconsider x1 = x, y1 = y, z1 = z as Element of REAL n by Def6;
reconsider x2 = x1, y2 = y1, z2 = z1 as Element of n -tuples_on REAL by EUCLID:def_1;
A2: ( len x2 = n & len y2 = n ) by CARD_1:def_7;
A3: for k being Nat st k in dom (mlt (x1,x1)) holds
0 <= (mlt (x1,x1)) . k
proof
let k be Nat; ::_thesis: ( k in dom (mlt (x1,x1)) implies 0 <= (mlt (x1,x1)) . k )
assume  k in dom (mlt (x1,x1)) ; ::_thesis: 0 <= (mlt (x1,x1)) . k
 (mlt (x1,x1)) . k = (x1 . k) * (x1 . k) by RVSUM_1:59;
hence  0 <= (mlt (x1,x1)) . k by XREAL_1:63; ::_thesis: verum
end;
A4: x .|. x = (Euclid_scalar n) . (x,x) by Def6
.= Sum (mlt (x1,x1)) by Def5 ;
hence  0 <= x .|. x by A3, RVSUM_1:84; ::_thesis: ( ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
thus  ( x .|. x = 0 iff x = 0. (REAL-US n) ) ::_thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
proof
now__::_thesis:_(_x_.|._x_=_0_implies_not_x_<>_0._(REAL-US_n)_)
assume that
A5: x .|. x = 0 and
A6: x <> 0. (REAL-US n) ; ::_thesis: contradiction
 for k being Element of NAT st k in dom x2 holds
x2 . k = 0
proof
let k be Element of NAT ; ::_thesis: ( k in dom x2 implies x2 . k = 0 )
 dom multreal = [:REAL,REAL:] by FUNCT_2:def_1;
then  [:(rng x1),(rng x1):] c= dom multreal by ZFMISC_1:96;
then A7: dom (multreal .: (x1,x1)) = (dom x1) /\ (dom x1) by FUNCOP_1:69;
assume  k in dom x2 ; ::_thesis: x2 . k = 0
then A8: k in dom (mlt (x1,x1)) by A7, RVSUM_1:def_9;
then  0 <= (mlt (x1,x1)) . k by A3;
then  (mlt (x1,x1)) . k = 0 by A4, A3, A5, A8, RVSUM_1:85;
then  (x1 . k) ^2 = 0 by RVSUM_1:59;
hence  x2 . k = 0 by SQUARE_1:12; ::_thesis: verum
end;
then  x1 = n |-> 0 by A1, RFUNCT_4:4;
then  x = 0* n by EUCLID:def_4;
hence  contradiction by A6, Def6; ::_thesis: verum
end;
hence  ( x .|. x = 0 implies x = 0. (REAL-US n) ) ; ::_thesis: ( x = 0. (REAL-US n) implies x .|. x = 0 )
assume  x = 0. (REAL-US n) ; ::_thesis: x .|. x = 0
then x = 0* n by Def6
.= n |-> 0 by EUCLID:def_4 ;
then  mlt (x2,x2) = 0 * x2 by RVSUM_1:63
.= n |-> 0 by RVSUM_1:53 ;
hence  x .|. x = 0 by A4, RVSUM_1:81; ::_thesis: verum
end;
A9: len z2 = n by CARD_1:def_7;
thus x .|. y = (Euclid_scalar n) . (x,y) by Def6
.= Sum (mlt (y1,x1)) by Def5
.= (Euclid_scalar n) . (y,x) by Def5
.= y .|. x by Def6 ; ::_thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
A10: x .|. z = (Euclid_scalar n) . (x,z) by Def6
.= Sum (mlt (x1,z1)) by Def5 ;
 a * x is Element of REAL n by Def6;
then reconsider ax = a * x as Element of n -tuples_on REAL by EUCLID:def_1;
A11: for k being Nat st k in Seg n holds
ax . k = (a * x1) . k
proof
reconsider a = a as Element of REAL ;
let k be Nat; ::_thesis: ( k in Seg n implies ax . k = (a * x1) . k )
assume  k in Seg n ; ::_thesis: ax . k = (a * x1) . k
a * x = (Euclid_mult n) . (a,x1) by Def6
.= a * x1 by Def2 ;
hence  ax . k = (a * x1) . k ; ::_thesis: verum
end;
A12: y .|. z = (Euclid_scalar n) . (y,z) by Def6
.= Sum (mlt (y1,z1)) by Def5 ;
thus (x + y) .|. z = (Euclid_scalar n) . ((x + y),z) by Def6
.= (Euclid_scalar n) . (((Euclid_add n) . (x1,y1)),z1) by Def6
.= (Euclid_scalar n) . ((x1 + y1),z1) by Def1
.= Sum (mlt ((x1 + y1),z1)) by Def5
.= Sum ((mlt (x1,z1)) + (mlt (y1,z1))) by A2, A9, RVSUM_1:118
.= (Sum (mlt (x2,z2))) + (Sum (mlt (y2,z2))) by RVSUM_1:89
.= (x .|. z) + (y .|. z) by A10, A12 ; ::_thesis: (a * x) .|. y = a * (x .|. y)
thus (a * x) .|. y = (Euclid_scalar n) . ((a * x),y) by Def6
.= (Euclid_scalar n) . ((a * x1),y1) by A11, FINSEQ_2:119
.= Sum (mlt ((a * x1),y1)) by Def5
.= Sum (a * (mlt (x2,y2))) by RVSUM_1:65
.= a * (Sum (mlt (x2,y2))) by RVSUM_1:87
.= a * ((Euclid_scalar n) . (x1,y1)) by Def5
.= a * (x .|. y) by Def6 ; ::_thesis: verum
end;
hence  REAL-US n is RealUnitarySpace-like by BHSP_1:def_2; ::_thesis: ( REAL-US n is vector-distributive & REAL-US n is scalar-distributive & REAL-US n is scalar-associative & REAL-US n is scalar-unital & REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
A13: for a, b being real number
for v being VECTOR of (REAL-US n) holds (a * b) * v = a * (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of (REAL-US n) holds (a * b) * v = a * (b * v)
let v be VECTOR of (REAL-US n); ::_thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as Element of REAL n by Def6;
reconsider a = a, b = b as Real by XREAL_0:def_1;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def_1;
 b * v is Element of REAL n by Def6;
then reconsider bv = b * v as Element of n -tuples_on REAL by EUCLID:def_1;
 for k being Nat st k in Seg n holds
bv . k = (b * v1) . k
proof
reconsider b = b as Element of REAL ;
let k be Nat; ::_thesis: ( k in Seg n implies bv . k = (b * v1) . k )
assume  k in Seg n ; ::_thesis: bv . k = (b * v1) . k
b * v = (Euclid_mult n) . (b,v1) by Def6
.= b * v1 by Def2 ;
hence  bv . k = (b * v1) . k ; ::_thesis: verum
end;
then  b * v1 = b * v by FINSEQ_2:119;
then A14: a * (b * v) = (Euclid_mult n) . (a,(b * v1)) by Def6
.= a * (b * v2) by Def2 ;
(a * b) * v = (Euclid_mult n) . ((a * b),v1) by Def6
.= (a * b) * v2 by Def2
.= a * (b * v2) by RVSUM_1:49 ;
hence  (a * b) * v = a * (b * v) by A14; ::_thesis: verum
end;
A15: for a being real number
for v, w being VECTOR of (REAL-US n) holds a * (v + w) = (a * v) + (a * w)
proof
let a be real number ; ::_thesis: for v, w being VECTOR of (REAL-US n) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of (REAL-US n); ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as Element of REAL n by Def6;
reconsider a = a as Real by XREAL_0:def_1;
reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def_1;
 a * v is Element of REAL n by Def6;
then reconsider av = a * v as Element of n -tuples_on REAL by EUCLID:def_1;
A16: for k being Nat st k in Seg n holds
av . k = (a * v1) . k
proof
let k be Nat; ::_thesis: ( k in Seg n implies av . k = (a * v1) . k )
assume  k in Seg n ; ::_thesis: av . k = (a * v1) . k
a * v = (Euclid_mult n) . (a,v1) by Def6
.= a * v1 by Def2 ;
hence  av . k = (a * v1) . k ; ::_thesis: verum
end;
 a * w is Element of REAL n by Def6;
then reconsider aw = a * w as Element of n -tuples_on REAL by EUCLID:def_1;
 for k being Nat st k in Seg n holds
aw . k = (a * w1) . k
proof
reconsider a = a as Element of REAL ;
let k be Nat; ::_thesis: ( k in Seg n implies aw . k = (a * w1) . k )
assume  k in Seg n ; ::_thesis: aw . k = (a * w1) . k
a * w = (Euclid_mult n) . (a,w1) by Def6
.= a * w1 by Def2 ;
hence  aw . k = (a * w1) . k ; ::_thesis: verum
end;
then A17: ( a * v1 is Element of n -tuples_on REAL & a * w1 = a * w ) by EUCLID:def_1, FINSEQ_2:119;
A18: (a * v) + (a * w) = (Euclid_add n) . ((a * v),(a * w)) by Def6
.= (Euclid_add n) . ((a * v1),(a * w1)) by A16, A17, FINSEQ_2:119
.= (a * v2) + (a * w2) by Def1 ;
a * (v + w) = (Euclid_mult n) . (a,(v + w)) by Def6
.= (Euclid_mult n) . (a,((Euclid_add n) . (v1,w1))) by Def6
.= (Euclid_mult n) . (a,(v1 + w1)) by Def1
.= a * (v1 + w1) by Def2
.= (a * v2) + (a * w2) by RVSUM_1:51 ;
hence  a * (v + w) = (a * v) + (a * w) by A18; ::_thesis: verum
end;
A19: for a, b being real number
for v being VECTOR of (REAL-US n) holds (a + b) * v = (a * v) + (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of (REAL-US n) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (REAL-US n); ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as Element of REAL n by Def6;
reconsider a = a, b = b as Real by XREAL_0:def_1;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def_1;
A20: (a + b) * v = (Euclid_mult n) . ((a + b),v1) by Def6
.= (a + b) * v2 by Def2
.= (a * v1) + (b * v1) by RVSUM_1:50 ;
 a * v is Element of REAL n by Def6;
then reconsider av = a * v as Element of n -tuples_on REAL by EUCLID:def_1;
A21: for k being Nat st k in Seg n holds
av . k = (a * v1) . k
proof
reconsider a = a as Element of REAL ;
let k be Nat; ::_thesis: ( k in Seg n implies av . k = (a * v1) . k )
assume  k in Seg n ; ::_thesis: av . k = (a * v1) . k
a * v = (Euclid_mult n) . (a,v1) by Def6
.= a * v1 by Def2 ;
hence  av . k = (a * v1) . k ; ::_thesis: verum
end;
 b * v is Element of REAL n by Def6;
then reconsider bv = b * v as Element of n -tuples_on REAL by EUCLID:def_1;
 for k being Nat st k in Seg n holds
bv . k = (b * v1) . k
proof
reconsider b = b as Element of REAL ;
let k be Nat; ::_thesis: ( k in Seg n implies bv . k = (b * v1) . k )
assume  k in Seg n ; ::_thesis: bv . k = (b * v1) . k
b * v = (Euclid_mult n) . (b,v1) by Def6
.= b * v1 by Def2 ;
hence  bv . k = (b * v1) . k ; ::_thesis: verum
end;
then A22: ( a * v1 is Element of n -tuples_on REAL & b * v1 = b * v ) by EUCLID:def_1, FINSEQ_2:119;
(a * v) + (b * v) = (Euclid_add n) . ((a * v),(b * v)) by Def6
.= (Euclid_add n) . ((a * v1),(b * v1)) by A21, A22, FINSEQ_2:119
.= (a * v2) + (b * v2) by Def1 ;
hence  (a + b) * v = (a * v) + (b * v) by A20; ::_thesis: verum
end;
 for v being VECTOR of (REAL-US n) holds 1 * v = v
proof
let v be VECTOR of (REAL-US n); ::_thesis: 1 * v = v
reconsider v1 = v as Element of REAL n by Def6;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def_1;
1 * v = (Euclid_mult n) . (1,v1) by Def6
.= 1 * v2 by Def2
.= v2 by RVSUM_1:52 ;
hence  1 * v = v ; ::_thesis: verum
end;
hence  ( REAL-US n is vector-distributive & REAL-US n is scalar-distributive & REAL-US n is scalar-associative & REAL-US n is scalar-unital ) by A15, A19, A13, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: ( REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
thus  REAL-US n is Abelian ::_thesis: ( REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
proof
let v, w be VECTOR of (REAL-US n); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of REAL n by Def6;
thus v + w = (Euclid_add n) . (v,w) by Def6
.= (Euclid_add n) . (w1,v1) by BINOP_1:def_2
.= w + v by Def6 ; ::_thesis: verum
end;
 for u, v, w being Element of (REAL-US n) holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of (REAL-US n); ::_thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Element of REAL n by Def6;
reconsider u2 = u1, v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def_1;
A23: u + (v + w) = (Euclid_add n) . (u1,(v + w)) by Def6
.= (Euclid_add n) . (u2,((Euclid_add n) . (v2,w2))) by Def6
.= (Euclid_add n) . (u2,(v1 + w1)) by Def1 ;
(u + v) + w = (Euclid_add n) . ((u + v),w1) by Def6
.= (Euclid_add n) . (((Euclid_add n) . (u1,v1)),w1) by Def6
.= (Euclid_add n) . ((u1 + v1),w1) by Def1
.= (u1 + v1) + w2 by Def1
.= u2 + (v2 + w2) by RVSUM_1:15 ;
hence  (u + v) + w = u + (v + w) by A23, Def1; ::_thesis: verum
end;
hence  REAL-US n is add-associative by RLVECT_1:def_3; ::_thesis: ( REAL-US n is right_zeroed & REAL-US n is right_complementable )
 for v being Element of (REAL-US n) holds v + (0. (REAL-US n)) = v
proof
let v be Element of (REAL-US n); ::_thesis: v + (0. (REAL-US n)) = v
reconsider v1 = v as Element of REAL n by Def6;
v + (0. (REAL-US n)) = (Euclid_add n) . (v,(0. (REAL-US n))) by Def6
.= (Euclid_add n) . (v1,(0* n)) by Def6
.= v1 + (0* n) by Def1 ;
hence  v + (0. (REAL-US n)) = v by EUCLID_4:1; ::_thesis: verum
end;
hence  REAL-US n is right_zeroed by RLVECT_1:def_4; ::_thesis: REAL-US n is right_complementable
let v be Element of (REAL-US n); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v1 = v as Element of REAL n by Def6;
reconsider w = - v1 as Element of (REAL-US n) by Def6;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. (REAL-US n)
A24: n in NAT by ORDINAL1:def_12;
thus v + w = (Euclid_add n) . (v1,(- v1)) by Def6
.= v1 + (- v1) by Def1
.= 0* n by A24, EUCLIDLP:2
.= 0. (REAL-US n) by Def6 ; ::_thesis: verum
end;
end;

theorem Th13: :: REAL_NS1:13
for n being Nat
for a being Real
for x1, y1 being Point of (REAL-NS n)
for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
proof
let n be Nat; ::_thesis: for a being Real
for x1, y1 being Point of (REAL-NS n)
for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
let a be Real; ::_thesis: for x1, y1 being Point of (REAL-NS n)
for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
let x1, y1 be Point of (REAL-NS n); ::_thesis: for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
reconsider x = x1, y = y1 as Element of REAL n by Def4;
let x2, y2 be Point of (REAL-US n); ::_thesis: ( x1 = x2 & y1 = y2 implies ( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 ) )
assume that
A1: x1 = x2 and
A2: y1 = y2 ; ::_thesis: ( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
thus x1 + y1 = (Euclid_add n) . (x,y) by Def4
.= x2 + y2 by A1, A2, Def6 ; ::_thesis: ( - x1 = - x2 & a * x1 = a * x2 )
thus  - x1 = (- 1) * x1 by RLVECT_1:16
.= (Euclid_mult n) . ((- 1),x) by Def4
.= (- 1) * x2 by A1, Def6
.= - x2 by RLVECT_1:16 ; ::_thesis: a * x1 = a * x2
thus a * x1 = (Euclid_mult n) . (a,x) by Def4
.= a * x2 by A1, Def6 ; ::_thesis: verum
end;

theorem :: REAL_NS1:14
for n being Nat
for x1 being Point of (REAL-NS n)
for x2 being Point of (REAL-US n) st x1 = x2 holds
||.x1.|| ^2 = x2 .|. x2
proof
let n be Nat; ::_thesis: for x1 being Point of (REAL-NS n)
for x2 being Point of (REAL-US n) st x1 = x2 holds
||.x1.|| ^2 = x2 .|. x2
let x1 be Point of (REAL-NS n); ::_thesis: for x2 being Point of (REAL-US n) st x1 = x2 holds
||.x1.|| ^2 = x2 .|. x2
let x2 be Point of (REAL-US n); ::_thesis: ( x1 = x2 implies ||.x1.|| ^2 = x2 .|. x2 )
reconsider x = x1 as Element of REAL n by Def4;
assume A1: x1 = x2 ; ::_thesis: ||.x1.|| ^2 = x2 .|. x2
thus ||.x1.|| ^2 = |.x.| ^2 by Th1
.= |(x,x)| by EUCLID_2:4
.= Sum (mlt (x,x)) by RVSUM_1:def_16
.= (Euclid_scalar n) . (x,x) by Def5
.= x2 .|. x2 by A1, Def6 ; ::_thesis: verum
end;

theorem Th15: :: REAL_NS1:15
for n being Nat
for f being set holds
( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) )
proof
let n be Nat; ::_thesis: for f being set holds
( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) )
let f be set ; ::_thesis: ( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) )
the carrier of (REAL-NS n) = REAL n by Def4
.= the carrier of (REAL-US n) by Def6 ;
hence  ( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) ) ; ::_thesis: verum
end;

theorem Th16: :: REAL_NS1:16
for n being Nat
for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 holds
( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )
proof
let n be Nat; ::_thesis: for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 holds
( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )
let seq1 be sequence of (REAL-NS n); ::_thesis: for seq2 being sequence of (REAL-US n) st seq1 = seq2 holds
( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )
let seq2 be sequence of (REAL-US n); ::_thesis: ( seq1 = seq2 implies ( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) ) )
assume A1: seq1 = seq2 ; ::_thesis: ( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )
A2: the carrier of (REAL-NS n) = REAL n by Def4
.= the carrier of (REAL-US n) by Def6 ;
now__::_thesis:_(_seq1_is_convergent_implies_(_seq2_is_convergent_&_lim_seq2_=_lim_seq1_)_)
reconsider LIMIT = lim seq1 as Point of (REAL-US n) by A2;
assume A3: seq1 is convergent ; ::_thesis: ( seq2 is convergent & lim seq2 = lim seq1 )
then consider RNg being Point of (REAL-NS n) such that
A4: for r being Real st 0 < r holds
ex m being Element of NAT st
for k being Element of NAT st m <= k holds
||.((seq1 . k) - RNg).|| < r by NORMSP_1:def_6;
reconsider RUg = RNg as Point of (REAL-US n) by A2;
 for r being Real st 0 < r holds
ex m being Element of NAT st
for k being Element of NAT st m <= k holds
dist ((seq2 . k),RUg) < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for k being Element of NAT st m <= k holds
dist ((seq2 . k),RUg) < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for k being Element of NAT st m <= k holds
dist ((seq2 . k),RUg) < r
then consider m being Element of NAT  such that
A5: for k being Element of NAT st m <= k holds
||.((seq1 . k) - RNg).|| < r by A4;
take  m ; ::_thesis: for k being Element of NAT st m <= k holds
dist ((seq2 . k),RUg) < r
 for k being Element of NAT st m <= k holds
dist ((seq2 . k),RUg) < r
proof
let k be Element of NAT ; ::_thesis: ( m <= k implies dist ((seq2 . k),RUg) < r )
reconsider p = (seq1 . k) - RNg as Element of REAL n by Def4;
assume A6: m <= k ; ::_thesis: dist ((seq2 . k),RUg) < r
 - RNg = - RUg by Th13;
then A7: p = (seq2 . k) - RUg by A1, Th13;
||.((seq1 . k) - RNg).|| = |.p.| by Th1
.= sqrt |(p,p)| by EUCLID_2:5
.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def_16
.= sqrt ((Euclid_scalar n) . (p,p)) by Def5
.= ||.((seq2 . k) - RUg).|| by A7, Def6 ;
hence  dist ((seq2 . k),RUg) < r by A5, A6; ::_thesis: verum
end;
hence  for k being Element of NAT st m <= k holds
dist ((seq2 . k),RUg) < r ; ::_thesis: verum
end;
hence A8: seq2 is convergent by BHSP_2:def_1; ::_thesis: lim seq2 = lim seq1
 for r being Real st r > 0 holds
ex m being Element of NAT st
for k being Element of NAT st k >= m holds
dist ((seq2 . k),LIMIT) < r
proof
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for k being Element of NAT st k >= m holds
dist ((seq2 . k),LIMIT) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for k being Element of NAT st k >= m holds
dist ((seq2 . k),LIMIT) < r
then consider m being Element of NAT  such that
A9: for k being Element of NAT st m <= k holds
||.((seq1 . k) - (lim seq1)).|| < r by A3, NORMSP_1:def_7;
take  m ; ::_thesis: for k being Element of NAT st k >= m holds
dist ((seq2 . k),LIMIT) < r
 for k being Element of NAT st m <= k holds
dist ((seq2 . k),LIMIT) < r
proof
let k be Element of NAT ; ::_thesis: ( m <= k implies dist ((seq2 . k),LIMIT) < r )
reconsider p = (seq1 . k) - (lim seq1) as Element of REAL n by Def4;
assume A10: m <= k ; ::_thesis: dist ((seq2 . k),LIMIT) < r
 - (lim seq1) = - LIMIT by Th13;
then A11: p = (seq2 . k) - LIMIT by A1, Th13;
||.((seq1 . k) - (lim seq1)).|| = |.p.| by Th1
.= sqrt |(p,p)| by EUCLID_2:5
.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def_16
.= sqrt ((Euclid_scalar n) . (p,p)) by Def5
.= ||.((seq2 . k) - LIMIT).|| by A11, Def6 ;
hence  dist ((seq2 . k),LIMIT) < r by A9, A10; ::_thesis: verum
end;
hence  for k being Element of NAT st k >= m holds
dist ((seq2 . k),LIMIT) < r ; ::_thesis: verum
end;
hence  lim seq2 = lim seq1 by A8, BHSP_2:def_2; ::_thesis: verum
end;
hence  ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) ; ::_thesis: ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) )
now__::_thesis:_(_seq2_is_convergent_implies_(_seq1_is_convergent_&_lim_seq1_=_lim_seq2_)_)
reconsider LIMIT = lim seq2 as Point of (REAL-NS n) by A2;
assume A12: seq2 is convergent ; ::_thesis: ( seq1 is convergent & lim seq1 = lim seq2 )
then consider RUg being Point of (REAL-US n) such that
A13: for r being Real st 0 < r holds
ex m being Element of NAT st
for k being Element of NAT st m <= k holds
dist ((seq2 . k),RUg) < r by BHSP_2:def_1;
reconsider RNg = RUg as Point of (REAL-NS n) by A2;
 for r being Real st 0 < r holds
ex m being Element of NAT st
for k being Element of NAT st m <= k holds
||.((seq1 . k) - RNg).|| < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for k being Element of NAT st m <= k holds
||.((seq1 . k) - RNg).|| < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for k being Element of NAT st m <= k holds
||.((seq1 . k) - RNg).|| < r
then consider m being Element of NAT  such that
A14: for k being Element of NAT st m <= k holds
dist ((seq2 . k),RUg) < r by A13;
take  m ; ::_thesis: for k being Element of NAT st m <= k holds
||.((seq1 . k) - RNg).|| < r
 for k being Element of NAT st m <= k holds
||.((seq1 . k) - RNg).|| < r
proof
let k be Element of NAT ; ::_thesis: ( m <= k implies ||.((seq1 . k) - RNg).|| < r )
reconsider p = (seq2 . k) - RUg as Element of REAL n by Def6;
assume  m <= k ; ::_thesis: ||.((seq1 . k) - RNg).|| < r
then A15: dist ((seq2 . k),RUg) < r by A14;
 - RNg = - RUg by Th13;
then A16: p = (seq1 . k) - RNg by A1, Th13;
dist ((seq2 . k),RUg) = sqrt ((Euclid_scalar n) . (p,p)) by Def6
.= sqrt (Sum (mlt (p,p))) by Def5
.= sqrt |(p,p)| by RVSUM_1:def_16
.= |.p.| by EUCLID_2:5 ;
hence  ||.((seq1 . k) - RNg).|| < r by A15, A16, Th1; ::_thesis: verum
end;
hence  for k being Element of NAT st m <= k holds
||.((seq1 . k) - RNg).|| < r ; ::_thesis: verum
end;
hence A17: seq1 is convergent by NORMSP_1:def_6; ::_thesis: lim seq1 = lim seq2
 for r being Real st r > 0 holds
ex m being Element of NAT st
for k being Element of NAT st k >= m holds
||.((seq1 . k) - LIMIT).|| < r
proof
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for k being Element of NAT st k >= m holds
||.((seq1 . k) - LIMIT).|| < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for k being Element of NAT st k >= m holds
||.((seq1 . k) - LIMIT).|| < r
then consider m being Element of NAT  such that
A18: for k being Element of NAT st k >= m holds
dist ((seq2 . k),(lim seq2)) < r by A12, BHSP_2:def_2;
take  m ; ::_thesis: for k being Element of NAT st k >= m holds
||.((seq1 . k) - LIMIT).|| < r
let k be Element of NAT ; ::_thesis: ( k >= m implies ||.((seq1 . k) - LIMIT).|| < r )
assume  k >= m ; ::_thesis: ||.((seq1 . k) - LIMIT).|| < r
then A19: dist ((seq2 . k),(lim seq2)) < r by A18;
reconsider p = (seq2 . k) - (lim seq2) as Element of REAL n by Def6;
 - (lim seq2) = - LIMIT by Th13;
then A20: p = (seq1 . k) - LIMIT by A1, Th13;
dist ((seq2 . k),(lim seq2)) = sqrt ((Euclid_scalar n) . (p,p)) by Def6
.= sqrt (Sum (mlt (p,p))) by Def5
.= sqrt |(p,p)| by RVSUM_1:def_16
.= |.p.| by EUCLID_2:5 ;
hence  ||.((seq1 . k) - LIMIT).|| < r by A19, A20, Th1; ::_thesis: verum
end;
hence  lim seq1 = lim seq2 by A17, NORMSP_1:def_7; ::_thesis: verum
end;
hence  ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) ; ::_thesis: verum
end;

theorem :: REAL_NS1:17
for n being Nat
for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm holds
seq2 is Cauchy
proof
let n be Nat; ::_thesis: for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm holds
seq2 is Cauchy
let seq1 be sequence of (REAL-NS n); ::_thesis: for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm holds
seq2 is Cauchy
let seq2 be sequence of (REAL-US n); ::_thesis: ( seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm implies seq2 is Cauchy )
assume that
A1: seq1 = seq2 and
A2: seq1 is Cauchy_sequence_by_Norm ; ::_thesis: seq2 is Cauchy
let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((seq2 . b2),(seq2 . b3)) ) )
assume  r > 0 ; ::_thesis: ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((seq2 . b2),(seq2 . b3)) )
then consider k being Element of NAT  such that
A3: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r by A2, RSSPACE3:def_5;
take  k ; ::_thesis: for b1, b2 being Element of NAT holds
( not k <= b1 or not k <= b2 or not r <= dist ((seq2 . b1),(seq2 . b2)) )
let m1, m2 be Element of NAT ; ::_thesis: ( not k <= m1 or not k <= m2 or not r <= dist ((seq2 . m1),(seq2 . m2)) )
reconsider p = (seq2 . m1) - (seq2 . m2) as Element of REAL n by Def6;
 - (seq1 . m2) = - (seq2 . m2) by A1, Th13;
then  (seq1 . m1) + (- (seq1 . m2)) = (seq2 . m1) + (- (seq2 . m2)) by A1, Th13;
then A4: ||.((seq1 . m1) - (seq1 . m2)).|| = |.p.| by Th1
.= sqrt |(p,p)| by EUCLID_2:5
.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def_16
.= sqrt ((Euclid_scalar n) . (p,p)) by Def5
.= ||.((seq2 . m1) - (seq2 . m2)).|| by Def6 ;
assume  ( m1 >= k & m2 >= k ) ; ::_thesis: not r <= dist ((seq2 . m1),(seq2 . m2))
then  dist ((seq1 . m1),(seq1 . m2)) < r by A3;
hence  not r <= dist ((seq2 . m1),(seq2 . m2)) by A4; ::_thesis: verum
end;

theorem Th18: :: REAL_NS1:18
for n being Nat
for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds
seq1 is Cauchy_sequence_by_Norm
proof
let n be Nat; ::_thesis: for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds
seq1 is Cauchy_sequence_by_Norm
let seq1 be sequence of (REAL-NS n); ::_thesis: for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds
seq1 is Cauchy_sequence_by_Norm
let seq2 be sequence of (REAL-US n); ::_thesis: ( seq1 = seq2 & seq2 is Cauchy implies seq1 is Cauchy_sequence_by_Norm )
assume that
A1: seq1 = seq2 and
A2: seq2 is Cauchy ; ::_thesis: seq1 is Cauchy_sequence_by_Norm
let r be Real; :: according to RSSPACE3:def_5 ::_thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((seq1 . b2),(seq1 . b3)) ) )
assume  r > 0 ; ::_thesis: ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((seq1 . b2),(seq1 . b3)) )
then consider k being Element of NAT  such that
A3: for m1, m2 being Element of NAT st m1 >= k & m2 >= k holds
dist ((seq2 . m1),(seq2 . m2)) < r by A2, BHSP_3:def_1;
take  k ; ::_thesis: for b1, b2 being Element of NAT holds
( not k <= b1 or not k <= b2 or not r <= dist ((seq1 . b1),(seq1 . b2)) )
let m1, m2 be Element of NAT ; ::_thesis: ( not k <= m1 or not k <= m2 or not r <= dist ((seq1 . m1),(seq1 . m2)) )
reconsider p = (seq2 . m1) - (seq2 . m2) as Element of REAL n by Def6;
 - (seq1 . m2) = - (seq2 . m2) by A1, Th13;
then A4: p = (seq1 . m1) - (seq1 . m2) by A1, Th13;
assume  ( m1 >= k & m2 >= k ) ; ::_thesis: not r <= dist ((seq1 . m1),(seq1 . m2))
then A5: dist ((seq2 . m1),(seq2 . m2)) < r by A3;
||.((seq2 . m1) - (seq2 . m2)).|| = sqrt ((Euclid_scalar n) . (p,p)) by Def6
.= sqrt (Sum (mlt (p,p))) by Def5
.= sqrt |(p,p)| by RVSUM_1:def_16
.= |.p.| by EUCLID_2:5
.= ||.((seq1 . m1) - (seq1 . m2)).|| by A4, Th1 ;
hence  not r <= dist ((seq1 . m1),(seq1 . m2)) by A5; ::_thesis: verum
end;

registration
let n be Nat;
cluster REAL-US n ->  non empty strict complete ;
coherence
 REAL-US n is complete
proof
let seq be sequence of (REAL-US n); :: according to BHSP_3:def_4 ::_thesis: ( not seq is Cauchy or seq is convergent )
reconsider seq9 = seq as sequence of (REAL-NS n) by Th15;
assume  seq is Cauchy ; ::_thesis: seq is convergent
then  seq9 is convergent by Th12, Th18;
hence  seq is convergent by Th16; ::_thesis: verum
end;
end;