:: NORMSP_1 semantic presentation

begin

definition
attrc1 is strict ;
struct NORMSTR  ->  RLSStruct , N-ZeroStr ;
aggrNORMSTR(# carrier, ZeroF, addF, Mult, normF #) ->  NORMSTR ;
end;

registration
cluster non empty strict for NORMSTR ;
existence
 ex b1 being NORMSTR st
( not b1 is empty & b1 is strict )
proof
set A = the non empty set ;
set Z = the Element of the non empty set ;
set a = the BinOp of the non empty set ;
set M = the Function of [:REAL, the non empty set :], the non empty set ;
set n = the Function of the non empty set ,REAL;
take  NORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) ; ::_thesis: ( not NORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) is empty & NORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) is strict )
thus  not the carrier of NORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: NORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) is strict
thus  NORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) is strict ; ::_thesis: verum
end;
end;

  deffunc H1( NORMSTR ) ->  Element of the carrier of $1 = 0. $1;

set V = the RealLinearSpace;

Lm1:  the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}
by RLSUB_1:def_3;

reconsider niltonil = the carrier of ((0). the RealLinearSpace) --> 0 as Function of the carrier of ((0). the RealLinearSpace),REAL by FUNCOP_1:45;

 0. the RealLinearSpace is VECTOR of ((0). the RealLinearSpace)
by Lm1, TARSKI:def_1;

then Lm2:  niltonil . (0. the RealLinearSpace) = 0
by FUNCOP_1:7;

Lm3:  for u being VECTOR of ((0). the RealLinearSpace)
for a being Real holds niltonil . (a * u) = (abs a) * (niltonil . u)
proof
let u be VECTOR of ((0). the RealLinearSpace); ::_thesis: for a being Real holds niltonil . (a * u) = (abs a) * (niltonil . u)
let a be Real; ::_thesis: niltonil . (a * u) = (abs a) * (niltonil . u)
 niltonil . u = 0 by FUNCOP_1:7;
hence  niltonil . (a * u) = (abs a) * (niltonil . u) by FUNCOP_1:7; ::_thesis: verum
end;

Lm4:  for u, v being VECTOR of ((0). the RealLinearSpace) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
proof
let u, v be VECTOR of ((0). the RealLinearSpace); ::_thesis: niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
 ( u = 0. the RealLinearSpace & v = 0. the RealLinearSpace ) by Lm1, TARSKI:def_1;
hence  niltonil . (u + v) <= (niltonil . u) + (niltonil . v) by Lm1, Lm2, TARSKI:def_1; ::_thesis: verum
end;

reconsider X = NORMSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),niltonil #) as non empty NORMSTR ;

Lm5: now__::_thesis:_for_x,_y_being_Point_of_X
for_a_being_Real_holds_
(_(_||.x.||_=_0_implies_x_=_H1(X)_)_&_(_x_=_H1(X)_implies_||.x.||_=_0_)_&_||.(a_*_x).||_=_(abs_a)_*_||.x.||_&_||.(x_+_y).||_<=_||.x.||_+_||.y.||_)
let x, y be Point of X; ::_thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = H1(X) ) & ( x = H1(X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; ::_thesis: ( ( ||.x.|| = 0 implies x = H1(X) ) & ( x = H1(X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider u = x, w = y as VECTOR of ((0). the RealLinearSpace) ;
 H1(X) = 0. the RealLinearSpace by RLSUB_1:11;
hence  ( ||.x.|| = 0 iff x = H1(X) ) by Lm1, FUNCOP_1:7, TARSKI:def_1; ::_thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
 a * x = a * u ;
hence  ||.(a * x).|| = (abs a) * ||.x.|| by Lm3; ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
 x + y = u + w ;
hence  ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm4; ::_thesis: verum
end;

definition
let IT be non empty NORMSTR ;
attrIT is RealNormSpace-like  means :Def1: :: NORMSP_1:def 1
 for x, y being Point of IT
for a being Real holds
( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| );
end;

:: deftheorem Def1 defines RealNormSpace-like NORMSP_1:def_1_:_
 for IT being non empty NORMSTR holds
( IT is RealNormSpace-like iff for x, y being Point of IT
for a being Real holds
( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like for NORMSTR ;
existence
 ex b1 being non empty NORMSTR st
( b1 is reflexive & b1 is discerning & b1 is RealNormSpace-like & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof
take  X ; ::_thesis: ( X is reflexive & X is discerning & X is RealNormSpace-like & X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
thus  X is reflexive ::_thesis: ( X is discerning & X is RealNormSpace-like & X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
proof
thus  ||.(0. X).|| = 0 by Lm5; :: according to NORMSP_0:def_6 ::_thesis: verum
end;
thus  X is discerning by Lm5, NORMSP_0:def_5; ::_thesis: ( X is RealNormSpace-like & X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
thus  X is RealNormSpace-like by Def1, Lm5; ::_thesis: ( X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
thus  ( X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital ) ::_thesis: ( X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
proof
thus  for a being real number
for v, w being VECTOR of X holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( X is scalar-distributive & X is scalar-associative & X is scalar-unital )
proof
let a be real number ; ::_thesis: for v, w being VECTOR of X holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of X; ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider v9 = v, w9 = w as VECTOR of ((0). the RealLinearSpace) ;
thus a * (v + w) = a * (v9 + w9)
.= (a * v9) + (a * w9) by RLVECT_1:def_5
.= (a * v) + (a * w) ; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of X holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( X is scalar-associative & X is scalar-unital )
proof
let a, b be real number ; ::_thesis: for v being VECTOR of X holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of X; ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
thus (a + b) * v = (a + b) * v9
.= (a * v9) + (b * v9) by RLVECT_1:def_6
.= (a * v) + (b * v) ; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of X holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: X is scalar-unital
proof
let a, b be real number ; ::_thesis: for v being VECTOR of X holds (a * b) * v = a * (b * v)
let v be VECTOR of X; ::_thesis: (a * b) * v = a * (b * v)
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by RLVECT_1:def_7
.= a * (b * v) ; ::_thesis: verum
end;
let v be VECTOR of X; :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
thus 1 * v = 1 * v9
.= v by RLVECT_1:def_8 ; ::_thesis: verum
end;
A1: for x, y being VECTOR of X
for x9, y9 being VECTOR of ((0). the RealLinearSpace) st x = x9 & y = y9 holds
( x + y = x9 + y9 & ( for a being Real holds a * x = a * x9 ) ) ;
thus  for v, w being VECTOR of X holds v + w = w + v :: according to RLVECT_1:def_2 ::_thesis: ( X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
proof
let v, w be VECTOR of X; ::_thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of ((0). the RealLinearSpace) ;
thus v + w = w9 + v9 by A1
.= w + v ; ::_thesis: verum
end;
thus  for u, v, w being VECTOR of X holds (u + v) + w = u + (v + w) :: according to RLVECT_1:def_3 ::_thesis: ( X is right_zeroed & X is right_complementable & X is strict )
proof
let u, v, w be VECTOR of X; ::_thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as VECTOR of ((0). the RealLinearSpace) ;
thus (u + v) + w = (u9 + v9) + w9
.= u9 + (v9 + w9) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
thus  for v being VECTOR of X holds v + (0. X) = v :: according to RLVECT_1:def_4 ::_thesis: ( X is right_complementable & X is strict )
proof
let v be VECTOR of X; ::_thesis: v + (0. X) = v
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
thus v + (0. X) = v9 + (0. ((0). the RealLinearSpace))
.= v by RLVECT_1:4 ; ::_thesis: verum
end;
thus  X is right_complementable ::_thesis: X is strict
proof
let v be VECTOR of X; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v9 = v as VECTOR of ((0). the RealLinearSpace) ;
consider w9 being VECTOR of ((0). the RealLinearSpace) such that
A2: v9 + w9 = 0. ((0). the RealLinearSpace) by ALGSTR_0:def_11;
reconsider w = w9 as VECTOR of X ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. X
thus  v + w = 0. X by A2; ::_thesis: verum
end;
thus  X is strict ; ::_thesis: verum
end;
end;

definition
mode RealNormSpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;
end;


theorem :: NORMSP_1:1
for RNS being RealNormSpace holds ||.(0. RNS).|| = 0 ;

theorem Th2: :: NORMSP_1:2
for RNS being RealNormSpace
for x being Point of RNS holds ||.(- x).|| = ||.x.||
proof
let RNS be RealNormSpace; ::_thesis: for x being Point of RNS holds ||.(- x).|| = ||.x.||
let x be Point of RNS; ::_thesis: ||.(- x).|| = ||.x.||
A1: abs (- 1) = - (- 1) by ABSVALUE:def_1
.= 1 ;
||.(- x).|| = ||.((- 1) * x).|| by RLVECT_1:16
.= (abs (- 1)) * ||.x.|| by Def1 ;
hence  ||.(- x).|| = ||.x.|| by A1; ::_thesis: verum
end;

theorem Th3: :: NORMSP_1:3
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||
proof
let RNS be RealNormSpace; ::_thesis: for x, y being Point of RNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||
let x, y be Point of RNS; ::_thesis: ||.(x - y).|| <= ||.x.|| + ||.y.||
 ||.(x - y).|| <= ||.x.|| + ||.(- y).|| by Def1;
hence  ||.(x - y).|| <= ||.x.|| + ||.y.|| by Th2; ::_thesis: verum
end;

theorem Th4: :: NORMSP_1:4
for RNS being RealNormSpace
for x being Point of RNS holds 0 <= ||.x.||
proof
let RNS be RealNormSpace; ::_thesis: for x being Point of RNS holds 0 <= ||.x.||
let x be Point of RNS; ::_thesis: 0 <= ||.x.||
||.(x - x).|| = ||.H1(RNS).|| by RLVECT_1:15
.= 0 ;
then  0 <= (||.x.|| + ||.x.||) / 2 by Th3;
hence  0 <= ||.x.|| ; ::_thesis: verum
end;

registration
let RNS be RealNormSpace;
let x be Point of RNS;
cluster||.x.|| ->  non negative ;
coherence
 not ||.x.|| is negative by Th4;
end;

theorem :: NORMSP_1:5
for a, b being Real
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= ((abs a) * ||.x.||) + ((abs b) * ||.y.||)
proof
let a, b be Real; ::_thesis: for RNS being RealNormSpace
for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= ((abs a) * ||.x.||) + ((abs b) * ||.y.||)
let RNS be RealNormSpace; ::_thesis: for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= ((abs a) * ||.x.||) + ((abs b) * ||.y.||)
let x, y be Point of RNS; ::_thesis: ||.((a * x) + (b * y)).|| <= ((abs a) * ||.x.||) + ((abs b) * ||.y.||)
 ||.((a * x) + (b * y)).|| <= ||.(a * x).|| + ||.(b * y).|| by Def1;
then  ||.((a * x) + (b * y)).|| <= ((abs a) * ||.x.||) + ||.(b * y).|| by Def1;
hence  ||.((a * x) + (b * y)).|| <= ((abs a) * ||.x.||) + ((abs b) * ||.y.||) by Def1; ::_thesis: verum
end;

theorem Th6: :: NORMSP_1:6
for RNS being RealNormSpace
for x, y being Point of RNS holds
( ||.(x - y).|| = 0 iff x = y )
proof
let RNS be RealNormSpace; ::_thesis: for x, y being Point of RNS holds
( ||.(x - y).|| = 0 iff x = y )
let x, y be Point of RNS; ::_thesis: ( ||.(x - y).|| = 0 iff x = y )
 ( ||.(x - y).|| = 0 iff x - y = H1(RNS) ) by NORMSP_0:def_5;
hence  ( ||.(x - y).|| = 0 iff x = y ) by RLVECT_1:15, RLVECT_1:21; ::_thesis: verum
end;

theorem Th7: :: NORMSP_1:7
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.(x - y).|| = ||.(y - x).||
proof
let RNS be RealNormSpace; ::_thesis: for x, y being Point of RNS holds ||.(x - y).|| = ||.(y - x).||
let x, y be Point of RNS; ::_thesis: ||.(x - y).|| = ||.(y - x).||
 x - y = - (y - x) by RLVECT_1:33;
hence  ||.(x - y).|| = ||.(y - x).|| by Th2; ::_thesis: verum
end;

theorem Th8: :: NORMSP_1:8
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.x.|| - ||.y.|| <= ||.(x - y).||
proof
let RNS be RealNormSpace; ::_thesis: for x, y being Point of RNS holds ||.x.|| - ||.y.|| <= ||.(x - y).||
let x, y be Point of RNS; ::_thesis: ||.x.|| - ||.y.|| <= ||.(x - y).||
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - H1(RNS) by RLVECT_1:15
.= x by RLVECT_1:13 ;
then  ||.x.|| <= ||.(x - y).|| + ||.y.|| by Def1;
hence  ||.x.|| - ||.y.|| <= ||.(x - y).|| by XREAL_1:20; ::_thesis: verum
end;

theorem Th9: :: NORMSP_1:9
for RNS being RealNormSpace
for x, y being Point of RNS holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
proof
let RNS be RealNormSpace; ::_thesis: for x, y being Point of RNS holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
let x, y be Point of RNS; ::_thesis: abs (||.x.|| - ||.y.||) <= ||.(x - y).||
(y - x) + x = y - (x - x) by RLVECT_1:29
.= y - H1(RNS) by RLVECT_1:15
.= y by RLVECT_1:13 ;
then  ||.y.|| <= ||.(y - x).|| + ||.x.|| by Def1;
then  ||.y.|| - ||.x.|| <= ||.(y - x).|| by XREAL_1:20;
then  ||.y.|| - ||.x.|| <= ||.(x - y).|| by Th7;
then A1: - (||.y.|| - ||.x.||) >= - ||.(x - y).|| by XREAL_1:24;
 ||.x.|| - ||.y.|| <= ||.(x - y).|| by Th8;
hence  abs (||.x.|| - ||.y.||) <= ||.(x - y).|| by A1, ABSVALUE:5; ::_thesis: verum
end;

theorem Th10: :: NORMSP_1:10
for RNS being RealNormSpace
for x, z, y being Point of RNS holds ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||
proof
let RNS be RealNormSpace; ::_thesis: for x, z, y being Point of RNS holds ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||
let x, z, y be Point of RNS; ::_thesis: ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||
x - z = x + (H1(RNS) + (- z)) by RLVECT_1:4
.= x + (((- y) + y) + (- z)) by RLVECT_1:5
.= x + ((- y) + (y + (- z))) by RLVECT_1:def_3
.= (x - y) + (y - z) by RLVECT_1:def_3 ;
hence  ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).|| by Def1; ::_thesis: verum
end;

theorem :: NORMSP_1:11
for RNS being RealNormSpace
for x, y being Point of RNS st x <> y holds
||.(x - y).|| <> 0 by Th6;


theorem :: NORMSP_1:12
for f being Function
for RNS being non empty 1-sorted
for x being Element of RNS holds
( f is sequence of RNS iff ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) )
proof
let f be Function; ::_thesis: for RNS being non empty 1-sorted
for x being Element of RNS holds
( f is sequence of RNS iff ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) )
let RNS be non empty 1-sorted ; ::_thesis: for x being Element of RNS holds
( f is sequence of RNS iff ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) )
let x be Element of RNS; ::_thesis: ( f is sequence of RNS iff ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) )
thus  ( f is sequence of RNS implies ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) ) ::_thesis: ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) implies f is sequence of RNS )
proof
assume A1: f is sequence of RNS ; ::_thesis: ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) )
then A2: rng f c= the carrier of RNS by RELAT_1:def_19;
A3: dom f = NAT by A1, FUNCT_2:def_1;
 for d being set st d in NAT holds
f . d is Element of RNS
proof
let d be set ; ::_thesis: ( d in NAT implies f . d is Element of RNS )
assume  d in NAT ; ::_thesis: f . d is Element of RNS
then  f . d in rng f by A3, FUNCT_1:def_3;
hence  f . d is Element of RNS by A2; ::_thesis: verum
end;
hence  ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) by A1, FUNCT_2:def_1; ::_thesis: verum
end;
thus  ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) implies f is sequence of RNS ) ::_thesis: verum
proof
assume that
A4: dom f = NAT and
A5: for d being set st d in NAT holds
f . d is Element of RNS ; ::_thesis: f is sequence of RNS
 for s being set st s in rng f holds
s in the carrier of RNS
proof
let s be set ; ::_thesis: ( s in rng f implies s in the carrier of RNS )
assume  s in rng f ; ::_thesis: s in the carrier of RNS
then consider d being set  such that
A6: d in dom f and
A7: s = f . d by FUNCT_1:def_3;
 f . d is Element of RNS by A4, A5, A6;
hence  s in the carrier of RNS by A7; ::_thesis: verum
end;
then  rng f c= the carrier of RNS by TARSKI:def_3;
hence  f is sequence of RNS by A4, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;

theorem :: NORMSP_1:13
for RNS being non empty 1-sorted
for x being Element of RNS ex S being sequence of RNS st rng S = {x}
proof
let RNS be non empty 1-sorted ; ::_thesis: for x being Element of RNS ex S being sequence of RNS st rng S = {x}
let x be Element of RNS; ::_thesis: ex S being sequence of RNS st rng S = {x}
consider f being Function such that
A1: dom f = NAT and
A2: rng f = {x} by FUNCT_1:5;
reconsider f = f as sequence of RNS by A1, A2, FUNCT_2:def_1, RELSET_1:4;
take  f ; ::_thesis: rng f = {x}
thus  rng f = {x} by A2; ::_thesis: verum
end;

theorem :: NORMSP_1:14
for RNS being non empty 1-sorted
for S being sequence of RNS st ex x being Element of RNS st
for n being Nat holds S . n = x holds
ex x being Element of RNS st rng S = {x}
proof
let RNS be non empty 1-sorted ; ::_thesis: for S being sequence of RNS st ex x being Element of RNS st
for n being Nat holds S . n = x holds
ex x being Element of RNS st rng S = {x}
let S be sequence of RNS; ::_thesis: ( ex x being Element of RNS st
for n being Nat holds S . n = x implies ex x being Element of RNS st rng S = {x} )
given z being Element of RNS such that A1: for n being Nat holds S . n = z ; ::_thesis: ex x being Element of RNS st rng S = {x}
take x = z; ::_thesis: rng S = {x}
now__::_thesis:_for_s_being_set_st_s_in_{x}_holds_
s_in_rng_S
let s be set ; ::_thesis: ( s in {x} implies s in rng S )
assume  s in {x} ; ::_thesis: s in rng S
then A2: s = x by TARSKI:def_1;
now__::_thesis:_s_in_rng_S
assume A3: not s in rng S ; ::_thesis: contradiction
now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction
let n be Element of NAT ; ::_thesis: contradiction
 n in NAT ;
then  n in dom S by FUNCT_2:def_1;
then  S . n <> x by A2, A3, FUNCT_1:def_3;
hence  contradiction by A1; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
hence  s in rng S ; ::_thesis: verum
end;
then A4: {x} c= rng S by TARSKI:def_3;
now__::_thesis:_for_t_being_set_st_t_in_rng_S_holds_
t_in_{x}
let t be set ; ::_thesis: ( t in rng S implies t in {x} )
assume  t in rng S ; ::_thesis: t in {x}
then consider d being set  such that
A5: d in dom S and
A6: S . d = t by FUNCT_1:def_3;
 d in NAT by A5, FUNCT_2:def_1;
then  t = z by A1, A6;
hence  t in {x} by TARSKI:def_1; ::_thesis: verum
end;
then  rng S c= {x} by TARSKI:def_3;
hence  rng S = {x} by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: NORMSP_1:15
for RNS being non empty 1-sorted
for S being sequence of RNS st ex x being Element of RNS st rng S = {x} holds
for n being Element of NAT holds S . n = S . (n + 1)
proof
let RNS be non empty 1-sorted ; ::_thesis: for S being sequence of RNS st ex x being Element of RNS st rng S = {x} holds
for n being Element of NAT holds S . n = S . (n + 1)
let S be sequence of RNS; ::_thesis: ( ex x being Element of RNS st rng S = {x} implies for n being Element of NAT holds S . n = S . (n + 1) )
given z being Element of RNS such that A1: rng S = {z} ; ::_thesis: for n being Element of NAT holds S . n = S . (n + 1)
let n be Element of NAT ; ::_thesis: S . n = S . (n + 1)
 n in NAT ;
then  n in dom S by FUNCT_2:def_1;
then  S . n in {z} by A1, FUNCT_1:def_3;
then A2: S . n = z by TARSKI:def_1;
 n + 1 in NAT ;
then  n + 1 in dom S by FUNCT_2:def_1;
then  S . (n + 1) in {z} by A1, FUNCT_1:def_3;
hence  S . n = S . (n + 1) by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem :: NORMSP_1:16
for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n being Element of NAT holds S . n = S . (n + 1) ) holds
for n, k being Element of NAT holds S . n = S . (n + k)
proof
let RNS be non empty 1-sorted ; ::_thesis: for S being sequence of RNS st ( for n being Element of NAT holds S . n = S . (n + 1) ) holds
for n, k being Element of NAT holds S . n = S . (n + k)
let S be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S . n = S . (n + 1) ) implies for n, k being Element of NAT holds S . n = S . (n + k) )
assume A1: for n being Element of NAT holds S . n = S . (n + 1) ; ::_thesis: for n, k being Element of NAT holds S . n = S . (n + k)
let n be Element of NAT ; ::_thesis: for k being Element of NAT holds S . n = S . (n + k)
defpred S1[ Element of NAT ] means S . n = S . (n + $1);
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 S . (n + k) = S . ((n + k) + 1) by A1;
hence  S1[k + 1] by A3; ::_thesis: verum
end;
A4: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;

theorem :: NORMSP_1:17
for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n, k being Element of NAT holds S . n = S . (n + k) ) holds
for n, m being Element of NAT holds S . n = S . m
proof
let RNS be non empty 1-sorted ; ::_thesis: for S being sequence of RNS st ( for n, k being Element of NAT holds S . n = S . (n + k) ) holds
for n, m being Element of NAT holds S . n = S . m
let S be sequence of RNS; ::_thesis: ( ( for n, k being Element of NAT holds S . n = S . (n + k) ) implies for n, m being Element of NAT holds S . n = S . m )
assume A1: for n, k being Element of NAT holds S . n = S . (n + k) ; ::_thesis: for n, m being Element of NAT holds S . n = S . m
let n, m be Element of NAT ; ::_thesis: S . n = S . m
A2: now__::_thesis:_(_m_<=_n_implies_S_._n_=_S_._m_)
assume  m <= n ; ::_thesis: S . n = S . m
then consider k being Nat such that
A3: n = m + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 n = m + k by A3;
hence  S . n = S . m by A1; ::_thesis: verum
end;
now__::_thesis:_(_n_<=_m_implies_S_._n_=_S_._m_)
assume  n <= m ; ::_thesis: S . n = S . m
then consider k being Nat such that
A4: m = n + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 m = n + k by A4;
hence  S . n = S . m by A1; ::_thesis: verum
end;
hence  S . n = S . m by A2; ::_thesis: verum
end;

theorem :: NORMSP_1:18
for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n, m being Element of NAT holds S . n = S . m ) holds
ex x being Element of RNS st
for n being Nat holds S . n = x
proof
let RNS be non empty 1-sorted ; ::_thesis: for S being sequence of RNS st ( for n, m being Element of NAT holds S . n = S . m ) holds
ex x being Element of RNS st
for n being Nat holds S . n = x
let S be sequence of RNS; ::_thesis: ( ( for n, m being Element of NAT holds S . n = S . m ) implies ex x being Element of RNS st
for n being Nat holds S . n = x )
assume that
A1: for n, m being Element of NAT holds S . n = S . m and
A2: for x being Element of RNS ex n being Nat st S . n <> x ; ::_thesis: contradiction
now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction
let n be Element of NAT ; ::_thesis: contradiction
consider z being Element of RNS such that
A3: S . n = z ;
consider k being Nat such that
A4: S . k <> z by A2;
 k in NAT by ORDINAL1:def_12;
hence  contradiction by A1, A3, A4; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;

Lm6:  for RNS being non empty 1-sorted
for S being sequence of RNS
for n being Element of NAT holds S . n is Element of RNS
;

definition
let RNS be non empty 1-sorted ;
let S be sequence of RNS;
let n be Element of NAT ;
:: original: .
redefine funcS . n ->  Element of RNS;
coherence
 S . n is Element of RNS by Lm6;
end;

definition
let RNS be non empty addLoopStr ;
let S1, S2 be sequence of RNS;
funcS1 + S2 ->  sequence of RNS means :Def2: :: NORMSP_1:def 2
 for n being Element of NAT holds it . n = (S1 . n) + (S2 . n);
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (S1 . n) + (S2 . n)
proof
deffunc H2( Element of NAT ) ->  Element of the carrier of RNS = (S1 . $1) + (S2 . $1);
thus  ex S being sequence of RNS st
for n being Element of NAT holds S . n = H2(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (S1 . n) + (S2 . n) ) & ( for n being Element of NAT holds b2 . n = (S1 . n) + (S2 . n) ) holds
b1 = b2
proof
let S, T be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S . n = (S1 . n) + (S2 . n) ) & ( for n being Element of NAT holds T . n = (S1 . n) + (S2 . n) ) implies S = T )
assume that
A1: for n being Element of NAT holds S . n = (S1 . n) + (S2 . n) and
A2: for n being Element of NAT holds T . n = (S1 . n) + (S2 . n) ; ::_thesis: S = T
 for n being Element of NAT holds S . n = T . n
proof
let n be Element of NAT ; ::_thesis: S . n = T . n
 S . n = (S1 . n) + (S2 . n) by A1;
hence  S . n = T . n by A2; ::_thesis: verum
end;
hence  S = T by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines + NORMSP_1:def_2_:_
 for RNS being non empty addLoopStr
for S1, S2, b4 being sequence of RNS holds
( b4 = S1 + S2 iff for n being Element of NAT holds b4 . n = (S1 . n) + (S2 . n) );

definition
let RNS be non empty addLoopStr ;
let S1, S2 be sequence of RNS;
funcS1 - S2 ->  sequence of RNS means :Def3: :: NORMSP_1:def 3
 for n being Element of NAT holds it . n = (S1 . n) - (S2 . n);
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (S1 . n) - (S2 . n)
proof
deffunc H2( Element of NAT ) ->  Element of the carrier of RNS = (S1 . $1) - (S2 . $1);
thus  ex S being sequence of RNS st
for n being Element of NAT holds S . n = H2(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (S1 . n) - (S2 . n) ) & ( for n being Element of NAT holds b2 . n = (S1 . n) - (S2 . n) ) holds
b1 = b2
proof
let S, T be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S . n = (S1 . n) - (S2 . n) ) & ( for n being Element of NAT holds T . n = (S1 . n) - (S2 . n) ) implies S = T )
assume that
A1: for n being Element of NAT holds S . n = (S1 . n) - (S2 . n) and
A2: for n being Element of NAT holds T . n = (S1 . n) - (S2 . n) ; ::_thesis: S = T
 for n being Element of NAT holds S . n = T . n
proof
let n be Element of NAT ; ::_thesis: S . n = T . n
 S . n = (S1 . n) - (S2 . n) by A1;
hence  S . n = T . n by A2; ::_thesis: verum
end;
hence  S = T by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines - NORMSP_1:def_3_:_
 for RNS being non empty addLoopStr
for S1, S2, b4 being sequence of RNS holds
( b4 = S1 - S2 iff for n being Element of NAT holds b4 . n = (S1 . n) - (S2 . n) );

definition
let RNS be non empty addLoopStr ;
let S be sequence of RNS;
let x be Element of RNS;
funcS - x ->  sequence of RNS means :Def4: :: NORMSP_1:def 4
 for n being Element of NAT holds it . n = (S . n) - x;
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (S . n) - x
proof
deffunc H2( Element of NAT ) ->  Element of the carrier of RNS = (S . $1) - x;
thus  ex S being sequence of RNS st
for n being Element of NAT holds S . n = H2(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (S . n) - x ) & ( for n being Element of NAT holds b2 . n = (S . n) - x ) holds
b1 = b2
proof
let S1, S2 be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (S . n) - x ) & ( for n being Element of NAT holds S2 . n = (S . n) - x ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = (S . n) - x and
A2: for n being Element of NAT holds S2 . n = (S . n) - x ; ::_thesis: S1 = S2
 for n being Element of NAT holds S1 . n = S2 . n
proof
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
 S1 . n = (S . n) - x by A1;
hence  S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence  S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines - NORMSP_1:def_4_:_
 for RNS being non empty addLoopStr
for S being sequence of RNS
for x being Element of RNS
for b4 being sequence of RNS holds
( b4 = S - x iff for n being Element of NAT holds b4 . n = (S . n) - x );

definition
let RNS be non empty RLSStruct ;
let S be sequence of RNS;
let a be Real;
funca * S ->  sequence of RNS means :Def5: :: NORMSP_1:def 5
 for n being Element of NAT holds it . n = a * (S . n);
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = a * (S . n)
proof
deffunc H2( Element of NAT ) ->  Element of the carrier of RNS = a * (S . $1);
thus  ex S being sequence of RNS st
for n being Element of NAT holds S . n = H2(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = a * (S . n) ) & ( for n being Element of NAT holds b2 . n = a * (S . n) ) holds
b1 = b2
proof
let S1, S2 be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S1 . n = a * (S . n) ) & ( for n being Element of NAT holds S2 . n = a * (S . n) ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = a * (S . n) and
A2: for n being Element of NAT holds S2 . n = a * (S . n) ; ::_thesis: S1 = S2
 for n being Element of NAT holds S1 . n = S2 . n
proof
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
 S1 . n = a * (S . n) by A1;
hence  S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence  S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines * NORMSP_1:def_5_:_
 for RNS being non empty RLSStruct
for S being sequence of RNS
for a being Real
for b4 being sequence of RNS holds
( b4 = a * S iff for n being Element of NAT holds b4 . n = a * (S . n) );

definition
let RNS be RealNormSpace;
let S be sequence of RNS;
attrS is convergent  means :Def6: :: NORMSP_1:def 6
 ex g being Point of RNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r;
end;

:: deftheorem Def6 defines convergent NORMSP_1:def_6_:_
 for RNS being RealNormSpace
for S being sequence of RNS holds
( S is convergent iff ex g being Point of RNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r );

theorem Th19: :: NORMSP_1:19
for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
S1 + S2 is convergent
proof
let RNS be RealNormSpace; ::_thesis: for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
S1 + S2 is convergent
let S1, S2 be sequence of RNS; ::_thesis: ( S1 is convergent & S2 is convergent implies S1 + S2 is convergent )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; ::_thesis: S1 + S2 is convergent
consider g1 being Point of RNS such that
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S1 . n) - g1).|| < r by A1, Def6;
consider g2 being Point of RNS such that
A4: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S2 . n) - g2).|| < r by A2, Def6;
take g = g1 + g2; :: according to NORMSP_1:def_6 ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r )
assume A5: 0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r
then consider m1 being Element of NAT  such that
A6: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - g1).|| < r / 2 by A3, XREAL_1:215;
consider m2 being Element of NAT  such that
A7: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - g2).|| < r / 2 by A4, A5, XREAL_1:215;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - g).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S1 + S2) . n) - g).|| < r )
assume A8: k <= n ; ::_thesis: ||.(((S1 + S2) . n) - g).|| < r
 m2 <= k by NAT_1:12;
then  m2 <= n by A8, XXREAL_0:2;
then A9: ||.((S2 . n) - g2).|| < r / 2 by A7;
A10: ||.(((S1 + S2) . n) - g).|| = ||.((- (g1 + g2)) + ((S1 . n) + (S2 . n))).|| by Def2
.= ||.(((- g1) + (- g2)) + ((S1 . n) + (S2 . n))).|| by RLVECT_1:31
.= ||.(((S1 . n) + ((- g1) + (- g2))) + (S2 . n)).|| by RLVECT_1:def_3
.= ||.((((S1 . n) - g1) + (- g2)) + (S2 . n)).|| by RLVECT_1:def_3
.= ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| by RLVECT_1:def_3 ;
A11: ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| <= ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| by Def1;
 m1 <= m1 + m2 by NAT_1:12;
then  m1 <= n by A8, XXREAL_0:2;
then  ||.((S1 . n) - g1).|| < r / 2 by A6;
then  ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| < (r / 2) + (r / 2) by A9, XREAL_1:8;
hence  ||.(((S1 + S2) . n) - g).|| < r by A10, A11, XXREAL_0:2; ::_thesis: verum
end;

theorem Th20: :: NORMSP_1:20
for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
S1 - S2 is convergent
proof
let RNS be RealNormSpace; ::_thesis: for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
S1 - S2 is convergent
let S1, S2 be sequence of RNS; ::_thesis: ( S1 is convergent & S2 is convergent implies S1 - S2 is convergent )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; ::_thesis: S1 - S2 is convergent
consider g1 being Point of RNS such that
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S1 . n) - g1).|| < r by A1, Def6;
consider g2 being Point of RNS such that
A4: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S2 . n) - g2).|| < r by A2, Def6;
take g = g1 - g2; :: according to NORMSP_1:def_6 ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 - S2) . n) - g).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 - S2) . n) - g).|| < r )
assume A5: 0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 - S2) . n) - g).|| < r
then consider m1 being Element of NAT  such that
A6: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - g1).|| < r / 2 by A3, XREAL_1:215;
consider m2 being Element of NAT  such that
A7: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - g2).|| < r / 2 by A4, A5, XREAL_1:215;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - g).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S1 - S2) . n) - g).|| < r )
assume A8: k <= n ; ::_thesis: ||.(((S1 - S2) . n) - g).|| < r
 m2 <= k by NAT_1:12;
then  m2 <= n by A8, XXREAL_0:2;
then A9: ||.((S2 . n) - g2).|| < r / 2 by A7;
A10: ||.(((S1 - S2) . n) - g).|| = ||.(((S1 . n) - (S2 . n)) - (g1 - g2)).|| by Def3
.= ||.((((S1 . n) - (S2 . n)) - g1) + g2).|| by RLVECT_1:29
.= ||.(((S1 . n) - (g1 + (S2 . n))) + g2).|| by RLVECT_1:27
.= ||.((((S1 . n) - g1) - (S2 . n)) + g2).|| by RLVECT_1:27
.= ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| by RLVECT_1:29 ;
A11: ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| <= ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| by Th3;
 m1 <= m1 + m2 by NAT_1:12;
then  m1 <= n by A8, XXREAL_0:2;
then  ||.((S1 . n) - g1).|| < r / 2 by A6;
then  ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| < (r / 2) + (r / 2) by A9, XREAL_1:8;
hence  ||.(((S1 - S2) . n) - g).|| < r by A10, A11, XXREAL_0:2; ::_thesis: verum
end;

theorem Th21: :: NORMSP_1:21
for RNS being RealNormSpace
for x being Point of RNS
for S being sequence of RNS st S is convergent holds
S - x is convergent
proof
let RNS be RealNormSpace; ::_thesis: for x being Point of RNS
for S being sequence of RNS st S is convergent holds
S - x is convergent
let x be Point of RNS; ::_thesis: for S being sequence of RNS st S is convergent holds
S - x is convergent
let S be sequence of RNS; ::_thesis: ( S is convergent implies S - x is convergent )
assume  S is convergent ; ::_thesis: S - x is convergent
then consider g being Point of RNS such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r by Def6;
take h = g - x; :: according to NORMSP_1:def_6 ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S - x) . n) - h).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S - x) . n) - h).|| < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S - x) . n) - h).|| < r
then consider m1 being Element of NAT  such that
A2: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S - x) . n) - h).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S - x) . n) - h).|| < r )
assume  k <= n ; ::_thesis: ||.(((S - x) . n) - h).|| < r
then A3: ||.((S . n) - g).|| < r by A2;
||.((S . n) - g).|| = ||.(((S . n) - H1(RNS)) - g).|| by RLVECT_1:13
.= ||.(((S . n) - (x - x)) - g).|| by RLVECT_1:15
.= ||.((((S . n) - x) + x) - g).|| by RLVECT_1:29
.= ||.(((S . n) - x) + ((- g) + x)).|| by RLVECT_1:def_3
.= ||.(((S . n) - x) - h).|| by RLVECT_1:33 ;
hence  ||.(((S - x) . n) - h).|| < r by A3, Def4; ::_thesis: verum
end;

theorem Th22: :: NORMSP_1:22
for a being Real
for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
a * S is convergent
proof
let a be Real; ::_thesis: for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
a * S is convergent
let RNS be RealNormSpace; ::_thesis: for S being sequence of RNS st S is convergent holds
a * S is convergent
let S be sequence of RNS; ::_thesis: ( S is convergent implies a * S is convergent )
assume  S is convergent ; ::_thesis: a * S is convergent
then consider g being Point of RNS such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r by Def6;
take h = a * g; :: according to NORMSP_1:def_6 ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((a * S) . n) - h).|| < r
A2: now__::_thesis:_(_a_<>_0_implies_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((a_*_S)_._n)_-_h).||_<_r_)
A3: 0 / (abs a) = 0 ;
assume A4: a <> 0 ; ::_thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
then A5: 0 < abs a by COMPLEX1:47;
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
then consider m1 being Element of NAT  such that
A6: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r / (abs a) by A1, A5, A3, XREAL_1:74;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((a * S) . n) - h).|| < r )
assume  k <= n ; ::_thesis: ||.(((a * S) . n) - h).|| < r
then A7: ||.((S . n) - g).|| < r / (abs a) by A6;
A8: 0 <> abs a by A4, COMPLEX1:47;
A9: (abs a) * (r / (abs a)) = (abs a) * (((abs a) ") * r) by XCMPLX_0:def_9
.= ((abs a) * ((abs a) ")) * r
.= 1 * r by A8, XCMPLX_0:def_7
.= r ;
||.((a * (S . n)) - (a * g)).|| = ||.(a * ((S . n) - g)).|| by RLVECT_1:34
.= (abs a) * ||.((S . n) - g).|| by Def1 ;
then  ||.((a * (S . n)) - h).|| < r by A5, A7, A9, XREAL_1:68;
hence  ||.(((a * S) . n) - h).|| < r by Def5; ::_thesis: verum
end;
now__::_thesis:_(_a_=_0_implies_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((a_*_S)_._n)_-_h).||_<_r_)
assume A10: a = 0 ; ::_thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
then consider m1 being Element of NAT  such that
A11: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((a * S) . n) - h).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((a * S) . n) - h).|| < r )
assume  k <= n ; ::_thesis: ||.(((a * S) . n) - h).|| < r
then A12: ||.((S . n) - g).|| < r by A11;
||.((a * (S . n)) - (a * g)).|| = ||.((0 * (S . n)) - H1(RNS)).|| by A10, RLVECT_1:10
.= ||.(H1(RNS) - H1(RNS)).|| by RLVECT_1:10
.= ||.H1(RNS).|| by RLVECT_1:13
.= 0 ;
then  ||.((a * (S . n)) - h).|| < r by A12;
hence  ||.(((a * S) . n) - h).|| < r by Def5; ::_thesis: verum
end;
hence  for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((a * S) . n) - h).|| < r by A2; ::_thesis: verum
end;

theorem Th23: :: NORMSP_1:23
for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
||.S.|| is convergent
proof
let RNS be RealNormSpace; ::_thesis: for S being sequence of RNS st S is convergent holds
||.S.|| is convergent
let S be sequence of RNS; ::_thesis: ( S is convergent implies ||.S.|| is convergent )
assume  S is convergent ; ::_thesis: ||.S.|| is convergent
then consider g being Point of RNS such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r by Def6;
now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_((||.S.||_._n)_-_||.g.||)_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r )
assume A2: 0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r
now__::_thesis:_for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_((||.S.||_._n)_-_||.g.||)_<_r
let n be Element of NAT ; ::_thesis: ( k <= n implies abs ((||.S.|| . n) - ||.g.||) < r )
assume  k <= n ; ::_thesis: abs ((||.S.|| . n) - ||.g.||) < r
then A4: ||.((S . n) - g).|| < r by A3;
 abs (||.(S . n).|| - ||.g.||) <= ||.((S . n) - g).|| by Th9;
then  abs (||.(S . n).|| - ||.g.||) < r by A4, XXREAL_0:2;
hence  abs ((||.S.|| . n) - ||.g.||) < r by NORMSP_0:def_4; ::_thesis: verum
end;
hence  for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r ; ::_thesis: verum
end;
hence  ||.S.|| is convergent by SEQ_2:def_6; ::_thesis: verum
end;

definition
let RNS be RealNormSpace;
let S be sequence of RNS;
assume A1: S is convergent ;
func lim S ->  Point of RNS means :Def7: :: NORMSP_1:def 7
 for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - it).|| < r;
existence
 ex b1 being Point of RNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b1).|| < r by A1, Def6;
uniqueness
 for b1, b2 being Point of RNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b1).|| < r ) & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b2).|| < r ) holds
b1 = b2
proof
 for x, y being Point of RNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - y).|| < r ) holds
x = y
proof
given x, y being Point of RNS such that A2: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r and
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - y).|| < r and
A4: x <> y ; ::_thesis: contradiction
A5: ||.(x - y).|| <> 0 by A4, Th6;
then A6: 0 / 4 < ||.(x - y).|| / 4 by XREAL_1:74;
then consider m1 being Element of NAT  such that
A7: for n being Element of NAT st m1 <= n holds
||.((S . n) - x).|| < ||.(x - y).|| / 4 by A2;
consider m2 being Element of NAT  such that
A8: for n being Element of NAT st m2 <= n holds
||.((S . n) - y).|| < ||.(x - y).|| / 4 by A3, A6;
A9: now__::_thesis:_not_m2_<=_m1
 ||.(x - y).|| <= ||.(x - (S . m1)).|| + ||.((S . m1) - y).|| by Th10;
then A10: ||.(x - y).|| <= ||.((S . m1) - x).|| + ||.((S . m1) - y).|| by Th7;
assume  m2 <= m1 ; ::_thesis: contradiction
then A11: ||.((S . m1) - y).|| < ||.(x - y).|| / 4 by A8;
 ||.((S . m1) - x).|| < ||.(x - y).|| / 4 by A7;
then  ||.((S . m1) - x).|| + ||.((S . m1) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A11, XREAL_1:8;
then  not ||.(x - y).|| / 2 < ||.(x - y).|| by A10, XXREAL_0:2;
hence  contradiction by A5, XREAL_1:216; ::_thesis: verum
end;
now__::_thesis:_not_m1_<=_m2
 ||.(x - y).|| <= ||.(x - (S . m2)).|| + ||.((S . m2) - y).|| by Th10;
then A12: ||.(x - y).|| <= ||.((S . m2) - x).|| + ||.((S . m2) - y).|| by Th7;
assume  m1 <= m2 ; ::_thesis: contradiction
then A13: ||.((S . m2) - x).|| < ||.(x - y).|| / 4 by A7;
 ||.((S . m2) - y).|| < ||.(x - y).|| / 4 by A8;
then  ||.((S . m2) - x).|| + ||.((S . m2) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A13, XREAL_1:8;
then  not ||.(x - y).|| / 2 < ||.(x - y).|| by A12, XXREAL_0:2;
hence  contradiction by A5, XREAL_1:216; ::_thesis: verum
end;
hence  contradiction by A9; ::_thesis: verum
end;
hence  for b1, b2 being Point of RNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b1).|| < r ) & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b2).|| < r ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines lim NORMSP_1:def_7_:_
 for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
for b3 being Point of RNS holds
( b3 = lim S iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b3).|| < r );

theorem :: NORMSP_1:24
for RNS being RealNormSpace
for g being Point of RNS
for S being sequence of RNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
proof
let RNS be RealNormSpace; ::_thesis: for g being Point of RNS
for S being sequence of RNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
let g be Point of RNS; ::_thesis: for S being sequence of RNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
let S be sequence of RNS; ::_thesis: ( S is convergent & lim S = g implies ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )
assume that
A1: S is convergent and
A2: lim S = g ; ::_thesis: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
A3: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_((||.(S_-_g).||_._n)_-_0)_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0) < r )
assume A4: 0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2, A4, Def7;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0) < r
let n be Element of NAT ; ::_thesis: ( k <= n implies abs ((||.(S - g).|| . n) - 0) < r )
assume  k <= n ; ::_thesis: abs ((||.(S - g).|| . n) - 0) < r
then  ||.((S . n) - g).|| < r by A5;
then A6: ||.(((S . n) - g) - H1(RNS)).|| < r by RLVECT_1:13;
 abs (||.((S . n) - g).|| - ||.H1(RNS).||) <= ||.(((S . n) - g) - H1(RNS)).|| by Th9;
then  abs (||.((S . n) - g).|| - ||.H1(RNS).||) < r by A6, XXREAL_0:2;
then  abs (||.((S - g) . n).|| - 0) < r by Def4;
hence  abs ((||.(S - g).|| . n) - 0) < r by NORMSP_0:def_4; ::_thesis: verum
end;
 ||.(S - g).|| is convergent by A1, Th21, Th23;
hence  ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) by A3, SEQ_2:def_7; ::_thesis: verum
end;

theorem :: NORMSP_1:25
for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
lim (S1 + S2) = (lim S1) + (lim S2)
proof
let RNS be RealNormSpace; ::_thesis: for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
lim (S1 + S2) = (lim S1) + (lim S2)
let S1, S2 be sequence of RNS; ::_thesis: ( S1 is convergent & S2 is convergent implies lim (S1 + S2) = (lim S1) + (lim S2) )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; ::_thesis: lim (S1 + S2) = (lim S1) + (lim S2)
set g2 = lim S2;
set g1 = lim S1;
set g = (lim S1) + (lim S2);
A3: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((S1_+_S2)_._n)_-_((lim_S1)_+_(lim_S2))).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
then A4: 0 < r / 2 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - (lim S1)).|| < r / 2 by A1, Def7;
consider m2 being Element of NAT  such that
A6: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - (lim S2)).|| < r / 2 by A2, A4, Def7;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r )
assume A7: k <= n ; ::_thesis: ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
 m2 <= k by NAT_1:12;
then  m2 <= n by A7, XXREAL_0:2;
then A8: ||.((S2 . n) - (lim S2)).|| < r / 2 by A6;
A9: ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| = ||.((- ((lim S1) + (lim S2))) + ((S1 . n) + (S2 . n))).|| by Def2
.= ||.(((- (lim S1)) + (- (lim S2))) + ((S1 . n) + (S2 . n))).|| by RLVECT_1:31
.= ||.(((S1 . n) + ((- (lim S1)) + (- (lim S2)))) + (S2 . n)).|| by RLVECT_1:def_3
.= ||.((((S1 . n) - (lim S1)) + (- (lim S2))) + (S2 . n)).|| by RLVECT_1:def_3
.= ||.(((S1 . n) - (lim S1)) + ((S2 . n) - (lim S2))).|| by RLVECT_1:def_3 ;
A10: ||.(((S1 . n) - (lim S1)) + ((S2 . n) - (lim S2))).|| <= ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| by Def1;
 m1 <= m1 + m2 by NAT_1:12;
then  m1 <= n by A7, XXREAL_0:2;
then  ||.((S1 . n) - (lim S1)).|| < r / 2 by A5;
then  ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence  ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r by A9, A10, XXREAL_0:2; ::_thesis: verum
end;
 S1 + S2 is convergent by A1, A2, Th19;
hence  lim (S1 + S2) = (lim S1) + (lim S2) by A3, Def7; ::_thesis: verum
end;

theorem :: NORMSP_1:26
for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
lim (S1 - S2) = (lim S1) - (lim S2)
proof
let RNS be RealNormSpace; ::_thesis: for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
lim (S1 - S2) = (lim S1) - (lim S2)
let S1, S2 be sequence of RNS; ::_thesis: ( S1 is convergent & S2 is convergent implies lim (S1 - S2) = (lim S1) - (lim S2) )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; ::_thesis: lim (S1 - S2) = (lim S1) - (lim S2)
set g2 = lim S2;
set g1 = lim S1;
set g = (lim S1) - (lim S2);
A3: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((S1_-_S2)_._n)_-_((lim_S1)_-_(lim_S2))).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
then A4: 0 < r / 2 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - (lim S1)).|| < r / 2 by A1, Def7;
consider m2 being Element of NAT  such that
A6: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - (lim S2)).|| < r / 2 by A2, A4, Def7;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r )
assume A7: k <= n ; ::_thesis: ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
 m2 <= k by NAT_1:12;
then  m2 <= n by A7, XXREAL_0:2;
then A8: ||.((S2 . n) - (lim S2)).|| < r / 2 by A6;
A9: ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| = ||.(((S1 . n) - (S2 . n)) - ((lim S1) - (lim S2))).|| by Def3
.= ||.((((S1 . n) - (S2 . n)) - (lim S1)) + (lim S2)).|| by RLVECT_1:29
.= ||.(((S1 . n) - ((lim S1) + (S2 . n))) + (lim S2)).|| by RLVECT_1:27
.= ||.((((S1 . n) - (lim S1)) - (S2 . n)) + (lim S2)).|| by RLVECT_1:27
.= ||.(((S1 . n) - (lim S1)) - ((S2 . n) - (lim S2))).|| by RLVECT_1:29 ;
A10: ||.(((S1 . n) - (lim S1)) - ((S2 . n) - (lim S2))).|| <= ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| by Th3;
 m1 <= m1 + m2 by NAT_1:12;
then  m1 <= n by A7, XXREAL_0:2;
then  ||.((S1 . n) - (lim S1)).|| < r / 2 by A5;
then  ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence  ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r by A9, A10, XXREAL_0:2; ::_thesis: verum
end;
 S1 - S2 is convergent by A1, A2, Th20;
hence  lim (S1 - S2) = (lim S1) - (lim S2) by A3, Def7; ::_thesis: verum
end;

theorem :: NORMSP_1:27
for RNS being RealNormSpace
for x being Point of RNS
for S being sequence of RNS st S is convergent holds
lim (S - x) = (lim S) - x
proof
let RNS be RealNormSpace; ::_thesis: for x being Point of RNS
for S being sequence of RNS st S is convergent holds
lim (S - x) = (lim S) - x
let x be Point of RNS; ::_thesis: for S being sequence of RNS st S is convergent holds
lim (S - x) = (lim S) - x
let S be sequence of RNS; ::_thesis: ( S is convergent implies lim (S - x) = (lim S) - x )
set g = lim S;
set h = (lim S) - x;
assume A1: S is convergent ; ::_thesis: lim (S - x) = (lim S) - x
A2: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((S_-_x)_._n)_-_((lim_S)_-_x)).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S - x) . n) - ((lim S) - x)).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S - x) . n) - ((lim S) - x)).|| < r
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st m1 <= n holds
||.((S . n) - (lim S)).|| < r by A1, Def7;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S - x) . n) - ((lim S) - x)).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S - x) . n) - ((lim S) - x)).|| < r )
assume  k <= n ; ::_thesis: ||.(((S - x) . n) - ((lim S) - x)).|| < r
then A4: ||.((S . n) - (lim S)).|| < r by A3;
||.((S . n) - (lim S)).|| = ||.(((S . n) - H1(RNS)) - (lim S)).|| by RLVECT_1:13
.= ||.(((S . n) - (x - x)) - (lim S)).|| by RLVECT_1:15
.= ||.((((S . n) - x) + x) - (lim S)).|| by RLVECT_1:29
.= ||.(((S . n) - x) + ((- (lim S)) + x)).|| by RLVECT_1:def_3
.= ||.(((S . n) - x) - ((lim S) - x)).|| by RLVECT_1:33 ;
hence  ||.(((S - x) . n) - ((lim S) - x)).|| < r by A4, Def4; ::_thesis: verum
end;
 S - x is convergent by A1, Th21;
hence  lim (S - x) = (lim S) - x by A2, Def7; ::_thesis: verum
end;

theorem :: NORMSP_1:28
for a being Real
for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
lim (a * S) = a * (lim S)
proof
let a be Real; ::_thesis: for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
lim (a * S) = a * (lim S)
let RNS be RealNormSpace; ::_thesis: for S being sequence of RNS st S is convergent holds
lim (a * S) = a * (lim S)
let S be sequence of RNS; ::_thesis: ( S is convergent implies lim (a * S) = a * (lim S) )
set g = lim S;
set h = a * (lim S);
assume A1: S is convergent ; ::_thesis: lim (a * S) = a * (lim S)
A2: now__::_thesis:_(_a_=_0_implies_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((a_*_S)_._n)_-_(a_*_(lim_S))).||_<_r_)
assume A3: a = 0 ; ::_thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r
then consider m1 being Element of NAT  such that
A4: for n being Element of NAT st m1 <= n holds
||.((S . n) - (lim S)).|| < r by A1, Def7;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((a * S) . n) - (a * (lim S))).|| < r )
assume  k <= n ; ::_thesis: ||.(((a * S) . n) - (a * (lim S))).|| < r
then A5: ||.((S . n) - (lim S)).|| < r by A4;
||.((a * (S . n)) - (a * (lim S))).|| = ||.((0 * (S . n)) - H1(RNS)).|| by A3, RLVECT_1:10
.= ||.(H1(RNS) - H1(RNS)).|| by RLVECT_1:10
.= ||.H1(RNS).|| by RLVECT_1:13
.= 0 ;
then  ||.((a * (S . n)) - (a * (lim S))).|| < r by A5;
hence  ||.(((a * S) . n) - (a * (lim S))).|| < r by Def5; ::_thesis: verum
end;
A6: now__::_thesis:_(_a_<>_0_implies_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((a_*_S)_._n)_-_(a_*_(lim_S))).||_<_r_)
A7: 0 / (abs a) = 0 ;
assume A8: a <> 0 ; ::_thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r
then A9: 0 < abs a by COMPLEX1:47;
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r
then  0 < r / (abs a) by A9, A7, XREAL_1:74;
then consider m1 being Element of NAT  such that
A10: for n being Element of NAT st m1 <= n holds
||.((S . n) - (lim S)).|| < r / (abs a) by A1, Def7;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((a * S) . n) - (a * (lim S))).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((a * S) . n) - (a * (lim S))).|| < r )
assume  k <= n ; ::_thesis: ||.(((a * S) . n) - (a * (lim S))).|| < r
then A11: ||.((S . n) - (lim S)).|| < r / (abs a) by A10;
A12: 0 <> abs a by A8, COMPLEX1:47;
A13: (abs a) * (r / (abs a)) = (abs a) * (((abs a) ") * r) by XCMPLX_0:def_9
.= ((abs a) * ((abs a) ")) * r
.= 1 * r by A12, XCMPLX_0:def_7
.= r ;
||.((a * (S . n)) - (a * (lim S))).|| = ||.(a * ((S . n) - (lim S))).|| by RLVECT_1:34
.= (abs a) * ||.((S . n) - (lim S)).|| by Def1 ;
then  ||.((a * (S . n)) - (a * (lim S))).|| < r by A9, A11, A13, XREAL_1:68;
hence  ||.(((a * S) . n) - (a * (lim S))).|| < r by Def5; ::_thesis: verum
end;
 a * S is convergent by A1, Th22;
hence  lim (a * S) = a * (lim S) by A2, A6, Def7; ::_thesis: verum
end;