let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace st Y is complete holds
for seq being sequence of st seq is Cauchy_sequence_by_Norm holds
seq is convergent

let Y be RealNormSpace; :: thesis: ( Y is complete implies for seq being sequence of st seq is Cauchy_sequence_by_Norm holds
seq is convergent )

assume A1: Y is complete ; :: thesis: for seq being sequence of st seq is Cauchy_sequence_by_Norm holds
seq is convergent

let vseq be sequence of ; :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A2: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent
defpred S1[ set , set ] means ex xseq being sequence of Y st
( ( for n being Nat holds xseq . n = (modetrans ((vseq . n),X,Y)) . \$1 ) & xseq is convergent & \$2 = lim xseq );
A3: for x being Element of () ex y being Element of Y st S1[x,y]
proof
let x be Element of (); :: thesis: ex y being Element of Y st S1[x,y]
deffunc H1( Nat) -> Element of the carrier of Y = (modetrans ((vseq . \$1),X,Y)) . x;
consider xseq being sequence of Y such that
A4: for n being Element of NAT holds xseq . n = H1(n) from A5: for n being Nat holds xseq . n = H1(n)
proof
let n be Nat; :: thesis: xseq . n = H1(n)
n in NAT by ORDINAL1:def 12;
hence xseq . n = H1(n) by A4; :: thesis: verum
end;
take lim xseq ; :: thesis: S1[x, lim xseq]
A6: for m, k being Nat holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ()
proof
let m, k be Nat; :: thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ()
reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
k in NAT by ORDINAL1:def 12;
then A7: xseq . k = (modetrans ((vseq . k),X,Y)) . x by A4;
a8: vseq . m is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
a9: vseq . k is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
m in NAT by ORDINAL1:def 12;
then xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4;
then (xseq . m) - (xseq . k) = h1 . x by ;
hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * () by LOPBAN10:45; :: thesis: verum
end;
now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e )

assume A10: e > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e

now :: thesis: ( ( ex i being Element of dom X st x . i = 0. (X . i) & ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ) or ( ( for i being Element of dom X holds not x . i = 0. (X . i) ) & ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ) )
per cases ( ex i being Element of dom X st x . i = 0. (X . i) or for i being Element of dom X holds not x . i = 0. (X . i) ) ;
case A11: ex i being Element of dom X st x . i = 0. (X . i) ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e

reconsider k = 0 as Nat ;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e

thus for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e :: thesis: verum
proof
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume that
n >= k and
m >= k ; :: thesis: ||.((xseq . n) - (xseq . m)).|| < e
m in NAT by ORDINAL1:def 12;
then A12: xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4
.= 0. Y by ;
n in NAT by ORDINAL1:def 12;
then xseq . n = (modetrans ((vseq . n),X,Y)) . x by A4
.= 0. Y by ;
hence ||.((xseq . n) - (xseq . m)).|| < e by ; :: thesis: verum
end;
end;
case for i being Element of dom X holds not x . i = 0. (X . i) ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e

then A13: NrProduct x > 0 by LOPBAN10:27;
then consider k being Nat such that
A15: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e / () by ;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e

thus for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e :: thesis: verum
proof
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume that
A16: n >= k and
A17: m >= k ; :: thesis: ||.((xseq . n) - (xseq . m)).|| < e
||.((vseq . n) - (vseq . m)).|| < e / () by ;
then A18: ||.((vseq . n) - (vseq . m)).|| * () < (e / ()) * () by ;
A19: (e / ()) * () = e * ((() ") * ())
.= e * 1 by
.= e ;
||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * () by A6;
hence ||.((xseq . n) - (xseq . m)).|| < e by ; :: thesis: verum
end;
end;
end;
end;
hence ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ; :: thesis: verum
end;
then xseq is Cauchy_sequence_by_Norm by RSSPACE3:8;
hence S1[x, lim xseq] by A1, A5; :: thesis: verum
end;
consider f being Function of the carrier of (), the carrier of Y such that
A20: for x being Element of () holds S1[x,f . x] from reconsider tseq = f as Function of (),Y ;
A21: for u being Point of ()
for i being Element of dom X
for x being Point of (X . i) ex xseqi being sequence of Y st
( ( for n being Nat holds xseqi . n = ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x ) & xseqi is convergent & (tseq * (reproj (i,u))) . x = lim xseqi )
proof
let u be Point of (); :: thesis: for i being Element of dom X
for x being Point of (X . i) ex xseqi being sequence of Y st
( ( for n being Nat holds xseqi . n = ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x ) & xseqi is convergent & (tseq * (reproj (i,u))) . x = lim xseqi )

let i be Element of dom X; :: thesis: for x being Point of (X . i) ex xseqi being sequence of Y st
( ( for n being Nat holds xseqi . n = ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x ) & xseqi is convergent & (tseq * (reproj (i,u))) . x = lim xseqi )

let x be Point of (X . i); :: thesis: ex xseqi being sequence of Y st
( ( for n being Nat holds xseqi . n = ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x ) & xseqi is convergent & (tseq * (reproj (i,u))) . x = lim xseqi )

reconsider v = (reproj (i,u)) . x as Point of () ;
consider xseq being sequence of Y such that
A22: ( ( for n being Nat holds xseq . n = (modetrans ((vseq . n),X,Y)) . v ) & xseq is convergent & tseq . v = lim xseq ) by A20;
A23: dom (reproj (i,u)) = the carrier of (X . i) by FUNCT_2:def 1;
take xseq ; :: thesis: ( ( for n being Nat holds xseq . n = ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x ) & xseq is convergent & (tseq * (reproj (i,u))) . x = lim xseq )
thus for n being Nat holds xseq . n = ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x :: thesis: ( xseq is convergent & (tseq * (reproj (i,u))) . x = lim xseq )
proof
let n be Nat; :: thesis: xseq . n = ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x
thus xseq . n = (modetrans ((vseq . n),X,Y)) . v by A22
.= (vseq . n) . ((reproj (i,u)) . x) by LOPBAN10:def 13
.= ((vseq . n) * (reproj (i,u))) . x by
.= ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x by LOPBAN10:def 13 ; :: thesis: verum
end;
thus xseq is convergent by A22; :: thesis: (tseq * (reproj (i,u))) . x = lim xseq
thus (tseq * (reproj (i,u))) . x = lim xseq by ; :: thesis: verum
end;
now :: thesis: for i being Element of dom X
for u being Point of () holds tseq * (reproj (i,u)) is LinearOperator of (X . i),Y
let i be Element of dom X; :: thesis: for u being Point of () holds tseq * (reproj (i,u)) is LinearOperator of (X . i),Y
let u be Point of (); :: thesis: tseq * (reproj (i,u)) is LinearOperator of (X . i),Y
set tseqiu = tseq * (reproj (i,u));
deffunc H1( Nat) -> Element of K16(K17( the carrier of (X . i), the carrier of Y)) = (modetrans ((vseq . \$1),X,Y)) * (reproj (i,u));
A24: now :: thesis: for x, y being Point of (X . i) holds (tseq * (reproj (i,u))) . (x + y) = ((tseq * (reproj (i,u))) . x) + ((tseq * (reproj (i,u))) . y)
let x, y be Point of (X . i); :: thesis: (tseq * (reproj (i,u))) . (x + y) = ((tseq * (reproj (i,u))) . x) + ((tseq * (reproj (i,u))) . y)
consider xseq being sequence of Y such that
A25: for n being Nat holds xseq . n = H1(n) . x and
A26: xseq is convergent and
A27: (tseq * (reproj (i,u))) . x = lim xseq by A21;
consider zseq being sequence of Y such that
A28: for n being Nat holds zseq . n = H1(n) . (x + y) and
zseq is convergent and
A29: (tseq * (reproj (i,u))) . (x + y) = lim zseq by A21;
consider yseq being sequence of Y such that
A30: for n being Nat holds yseq . n = H1(n) . y and
A31: yseq is convergent and
A32: (tseq * (reproj (i,u))) . y = lim yseq by A21;
now :: thesis: for n being Nat holds zseq . n = (xseq . n) + (yseq . n)
let n be Nat; :: thesis: zseq . n = (xseq . n) + (yseq . n)
A33: H1(n) is LinearOperator of (X . i),Y by LOPBAN10:def 6;
thus zseq . n = H1(n) . (x + y) by A28
.= (H1(n) . x) + (H1(n) . y) by
.= (xseq . n) + (H1(n) . y) by A25
.= (xseq . n) + (yseq . n) by A30 ; :: thesis: verum
end;
then zseq = xseq + yseq by NORMSP_1:def 2;
hence (tseq * (reproj (i,u))) . (x + y) = ((tseq * (reproj (i,u))) . x) + ((tseq * (reproj (i,u))) . y) by ; :: thesis: verum
end;
now :: thesis: for x being Point of (X . i)
for a being Real holds (tseq * (reproj (i,u))) . (a * x) = a * ((tseq * (reproj (i,u))) . x)
let x be Point of (X . i); :: thesis: for a being Real holds (tseq * (reproj (i,u))) . (a * x) = a * ((tseq * (reproj (i,u))) . x)
let a be Real; :: thesis: (tseq * (reproj (i,u))) . (a * x) = a * ((tseq * (reproj (i,u))) . x)
consider xseq being sequence of Y such that
A34: for n being Nat holds xseq . n = H1(n) . x and
A35: xseq is convergent and
A36: (tseq * (reproj (i,u))) . x = lim xseq by A21;
consider zseq being sequence of Y such that
A37: for n being Nat holds zseq . n = H1(n) . (a * x) and
zseq is convergent and
A38: (tseq * (reproj (i,u))) . (a * x) = lim zseq by A21;
now :: thesis: for n being Nat holds zseq . n = a * (xseq . n)
let n be Nat; :: thesis: zseq . n = a * (xseq . n)
A39: H1(n) is LinearOperator of (X . i),Y by LOPBAN10:def 6;
thus zseq . n = H1(n) . (a * x) by A37
.= a * (H1(n) . x) by
.= a * (xseq . n) by A34 ; :: thesis: verum
end;
then zseq = a * xseq by NORMSP_1:def 5;
hence (tseq * (reproj (i,u))) . (a * x) = a * ((tseq * (reproj (i,u))) . x) by ; :: thesis: verum
end;
hence tseq * (reproj (i,u)) is LinearOperator of (X . i),Y by ; :: thesis: verum
end;
then reconsider tseq = tseq as MultilinearOperator of X,Y by LOPBAN10:def 6;
B39: now :: thesis: for e1 being Real st e1 > 0 holds
ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
let e1 be Real; :: thesis: ( e1 > 0 implies ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )

assume A40: e1 > 0 ; :: thesis: ex k being Nat st
for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

reconsider e = e1 as Real ;
consider k being Nat such that
A41: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by ;
reconsider k = k as Nat ;
take k = k; :: thesis: for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

now :: thesis: for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
let m be Nat; :: thesis: ( m >= k implies |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 )
assume m >= k ; :: thesis: |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1
then A42: ||.((vseq . m) - (vseq . k)).|| < e by A41;
A43: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def 4;
A44: ||.(vseq . k).|| = ||.vseq.|| . k by NORMSP_0:def 4;
|.(||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| by NORMSP_1:9;
hence |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 by ; :: thesis: verum
end;
hence for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 ; :: thesis: verum
end;
then A45: ||.vseq.|| is convergent by SEQ_4:41;
A46: tseq is Lipschitzian
proof
take lim ||.vseq.|| ; :: according to LOPBAN10:def 10 :: thesis: ( 0 <= lim ||.vseq.|| & ( for b1 being Element of the carrier of () holds ||.(tseq . b1).|| <= (lim ||.vseq.||) * () ) )
A47: now :: thesis: for x being Point of () holds ||.(tseq . x).|| <= (lim ||.vseq.||) * ()
let x be Point of (); :: thesis: ||.(tseq . x).|| <= (lim ||.vseq.||) * ()
consider xseq being sequence of Y such that
A48: for n being Nat holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A49: xseq is convergent and
A50: tseq . x = lim xseq by A20;
A51: ||.(tseq . x).|| = lim ||.xseq.|| by ;
A52: for m being Nat holds ||.(xseq . m).|| <= ||.(vseq . m).|| * ()
proof
let m be Nat; :: thesis: ||.(xseq . m).|| <= ||.(vseq . m).|| * ()
A53: xseq . m = (modetrans ((vseq . m),X,Y)) . x by A48;
vseq . m is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
hence ||.(xseq . m).|| <= ||.(vseq . m).|| * () by ; :: thesis: verum
end;
A54: for n being Nat holds ||.xseq.|| . n <= (() (#) ||.vseq.||) . n
proof
let n be Nat; :: thesis: ||.xseq.|| . n <= (() (#) ||.vseq.||) . n
A55: ||.xseq.|| . n = ||.(xseq . n).|| by NORMSP_0:def 4;
A56: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def 4;
||.(xseq . n).|| <= ||.(vseq . n).|| * () by A52;
hence ||.xseq.|| . n <= (() (#) ||.vseq.||) . n by ; :: thesis: verum
end;
A58: lim (() (#) ||.vseq.||) = (lim ||.vseq.||) * () by ;
||.xseq.|| is convergent by ;
hence ||.(tseq . x).|| <= (lim ||.vseq.||) * () by ; :: thesis: verum
end;
now :: thesis: for n being Nat holds ||.vseq.|| . n >= 0
let n be Nat; :: thesis: ||.vseq.|| . n >= 0
||.(vseq . n).|| >= 0 ;
hence ||.vseq.|| . n >= 0 by NORMSP_0:def 4; :: thesis: verum
end;
hence ( 0 <= lim ||.vseq.|| & ( for b1 being Element of the carrier of () holds ||.(tseq . b1).|| <= (lim ||.vseq.||) * () ) ) by ; :: thesis: verum
end;
A59: for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ()
proof
let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * () )

assume e > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ()

then consider k being Nat such that
A60: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by ;
take k ; :: thesis: for n being Nat st n >= k holds
for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ()

now :: thesis: for n being Nat st n >= k holds
for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ()
let n be Nat; :: thesis: ( n >= k implies for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * () )
assume A61: n >= k ; :: thesis: for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ()
now :: thesis: for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ()
let x be Point of (); :: thesis: ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ()
consider xseq being sequence of Y such that
A62: for n being Nat holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A63: xseq is convergent and
A64: tseq . x = lim xseq by A20;
A65: for m, k being Nat holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ()
proof
let m, k be Nat; :: thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ()
reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
A66: xseq . k = (modetrans ((vseq . k),X,Y)) . x by A62;
a67: vseq . m is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
a68: vseq . k is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
xseq . m = (modetrans ((vseq . m),X,Y)) . x by A62;
then (xseq . m) - (xseq . k) = h1 . x by ;
hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * () by LOPBAN10:45; :: thesis: verum
end;
A69: for m being Nat st m >= k holds
||.((xseq . n) - (xseq . m)).|| <= e * ()
proof
let m be Nat; :: thesis: ( m >= k implies ||.((xseq . n) - (xseq . m)).|| <= e * () )
assume m >= k ; :: thesis: ||.((xseq . n) - (xseq . m)).|| <= e * ()
then A70: ||.((vseq . n) - (vseq . m)).|| < e by ;
A71: ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * () by A65;
||.((vseq . n) - (vseq . m)).|| * () <= e * () by ;
hence ||.((xseq . n) - (xseq . m)).|| <= e * () by ; :: thesis: verum
end;
||.((xseq . n) - (tseq . x)).|| <= e * ()
proof
deffunc H1( Nat) -> object = ||.((xseq . \$1) - (xseq . n)).||;
consider rseq being Real_Sequence such that
A72: for m being Nat holds rseq . m = H1(m) from SEQ_1:sch 1();
now :: thesis: for x being object st x in NAT holds
rseq . x = ||.(xseq - (xseq . n)).|| . x
let x be object ; :: thesis: ( x in NAT implies rseq . x = ||.(xseq - (xseq . n)).|| . x )
assume x in NAT ; :: thesis: rseq . x = ||.(xseq - (xseq . n)).|| . x
then reconsider k = x as Nat ;
thus rseq . x = ||.((xseq . k) - (xseq . n)).|| by A72
.= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def 4
.= ||.(xseq - (xseq . n)).|| . x by NORMSP_0:def 4 ; :: thesis: verum
end;
then A73: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2:12;
A74: xseq - (xseq . n) is convergent by ;
lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) by ;
then A75: lim rseq = ||.((tseq . x) - (xseq . n)).|| by ;
for m being Nat st m >= k holds
rseq . m <= e * ()
proof
let m be Nat; :: thesis: ( m >= k implies rseq . m <= e * () )
assume A76: m >= k ; :: thesis: rseq . m <= e * ()
rseq . m = ||.((xseq . m) - (xseq . n)).|| by A72
.= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1:7 ;
hence rseq . m <= e * () by ; :: thesis: verum
end;
then lim rseq <= e * () by ;
hence ||.((xseq . n) - (tseq . x)).|| <= e * () by ; :: thesis: verum
end;
hence ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * () by A62; :: thesis: verum
end;
hence for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * () ; :: thesis: verum
end;
hence for n being Nat st n >= k holds
for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * () ; :: thesis: verum
end;
reconsider tseq = tseq as Lipschitzian MultilinearOperator of X,Y by A46;
reconsider tv = tseq as Point of by LOPBAN10:def 11;
A77: for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e
proof
let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e )

assume A78: e > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e

consider k being Nat such that
A79: for n being Nat st n >= k holds
for x being Point of () holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * () by ;
now :: thesis: for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e
set g1 = tseq;
let n be Nat; :: thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )
assume A80: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e
reconsider h1 = (vseq . n) - tv as Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
set f1 = modetrans ((vseq . n),X,Y);
A81: now :: thesis: for t being Point of () st ( for i being Element of dom X holds ||.(t . i).|| <= 1 ) holds
||.(h1 . t).|| <= e
let t be Point of (); :: thesis: ( ( for i being Element of dom X holds ||.(t . i).|| <= 1 ) implies ||.(h1 . t).|| <= e )
assume for i being Element of dom X holds ||.(t . i).|| <= 1 ; :: thesis: ||.(h1 . t).|| <= e
then ( 0 <= NrProduct t & NrProduct t <= 1 ) by LOPBAN10:35;
then A82: e * () <= e * 1 by ;
A83: ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| <= e * () by ;
vseq . n is Lipschitzian MultilinearOperator of X,Y by LOPBAN10:def 11;
then ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by LOPBAN10:52;
hence ||.(h1 . t).|| <= e by ; :: thesis: verum
end;
A84: now :: thesis: for r being Real st r in PreNorms h1 holds
r <= e
let r be Real; :: thesis: ( r in PreNorms h1 implies r <= e )
assume r in PreNorms h1 ; :: thesis: r <= e
then ex t being Point of () st
( r = ||.(h1 . t).|| & ( for i being Element of dom X holds ||.(t . i).|| <= 1 ) ) ;
hence r <= e by A81; :: thesis: verum
end;
( ( for s being Real st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;
hence ||.((vseq . n) - tv).|| <= e by ; :: thesis: verum
end;
hence ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e ; :: thesis: verum
end;
for e being Real st e > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; :: thesis: ( e > 0 implies ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e )

assume A86: e > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e

consider m being Nat such that
A87: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by ;
A88: e / 2 < e by ;
now :: thesis: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
let n be Nat; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq . n) - tv).|| <= e / 2 by A87;
hence ||.((vseq . n) - tv).|| < e by ; :: thesis: verum
end;
hence ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e ; :: thesis: verum
end;
hence vseq is convergent by NORMSP_1:def 6; :: thesis: verum