let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace st Y is complete holds

for seq being sequence of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent )

assume A1: Y is complete ; :: thesis: for seq being sequence of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

let vseq be sequence of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)); :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )

assume A2: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent

defpred S_{1}[ 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 (product X) ex y being Element of Y st S_{1}[x,y]

A20: for x being Element of (product X) holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A3);

reconsider tseq = f as Function of (product X),Y ;

A21: for u being Point of (product X)

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 )

A46: tseq is Lipschitzian

ex k being Nat st

for n being Nat st n >= k holds

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

reconsider tv = tseq as Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) 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

ex m being Nat st

for n being Nat st n >= m holds

||.((vseq . n) - tv).|| < e

for seq being sequence of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent )

assume A1: Y is complete ; :: thesis: for seq being sequence of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

let vseq be sequence of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)); :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )

assume A2: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent

defpred S

( ( 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 (product X) ex y being Element of Y st S

proof

consider f being Function of the carrier of (product X), the carrier of Y such that
let x be Element of (product X); :: thesis: ex y being Element of Y st S_{1}[x,y]

deffunc H_{1}( 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 = H_{1}(n)
from FUNCT_2:sch 4();

A5: for n being Nat holds xseq . n = H_{1}(n)
_{1}[x, lim xseq]

A6: for m, k being Nat holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (NrProduct x)

hence S_{1}[x, lim xseq]
by A1, A5; :: thesis: verum

end;deffunc H

consider xseq being sequence of Y such that

A4: for n being Element of NAT holds xseq . n = H

A5: for n being Nat holds xseq . n = H

proof

take
lim xseq
; :: thesis: S
let n be Nat; :: thesis: xseq . n = H_{1}(n)

n in NAT by ORDINAL1:def 12;

hence xseq . n = H_{1}(n)
by A4; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence xseq . n = H

A6: for m, k being Nat holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (NrProduct x)

proof

let m, k be Nat; :: thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (NrProduct x)

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 A7, a8, a9, LOPBAN10:52;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (NrProduct x) by LOPBAN10:45; :: thesis: verum

end;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 A7, a8, a9, LOPBAN10:52;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (NrProduct x) by LOPBAN10:45; :: thesis: verum

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

then
xseq is Cauchy_sequence_by_Norm
by RSSPACE3:8;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

for n, m being Nat st n >= k & m >= k holds

||.((xseq . n) - (xseq . m)).|| < e ; :: thesis: verum

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

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

end;

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

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

end;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 A11, LOPBAN10:36 ;

n in NAT by ORDINAL1:def 12;

then xseq . n = (modetrans ((vseq . n),X,Y)) . x by A4

.= 0. Y by A11, LOPBAN10:36 ;

hence ||.((xseq . n) - (xseq . m)).|| < e by A10, A12; :: thesis: verum

end;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 A11, LOPBAN10:36 ;

n in NAT by ORDINAL1:def 12;

then xseq . n = (modetrans ((vseq . n),X,Y)) . x by A4

.= 0. Y by A11, LOPBAN10:36 ;

hence ||.((xseq . n) - (xseq . m)).|| < e by A10, A12; :: thesis: verum

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

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 / (NrProduct x) by A2, A10, RSSPACE3:8;

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

end;then consider k being Nat such that

A15: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e / (NrProduct x) by A2, A10, RSSPACE3:8;

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 / (NrProduct x) by A15, A16, A17;

then A18: ||.((vseq . n) - (vseq . m)).|| * (NrProduct x) < (e / (NrProduct x)) * (NrProduct x) by A13, XREAL_1:68;

A19: (e / (NrProduct x)) * (NrProduct x) = e * (((NrProduct x) ") * (NrProduct x))

.= e * 1 by A13, XCMPLX_0:def 7

.= e ;

||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * (NrProduct x) by A6;

hence ||.((xseq . n) - (xseq . m)).|| < e by A18, A19, XXREAL_0:2; :: thesis: verum

end;assume that

A16: n >= k and

A17: m >= k ; :: thesis: ||.((xseq . n) - (xseq . m)).|| < e

||.((vseq . n) - (vseq . m)).|| < e / (NrProduct x) by A15, A16, A17;

then A18: ||.((vseq . n) - (vseq . m)).|| * (NrProduct x) < (e / (NrProduct x)) * (NrProduct x) by A13, XREAL_1:68;

A19: (e / (NrProduct x)) * (NrProduct x) = e * (((NrProduct x) ") * (NrProduct x))

.= e * 1 by A13, XCMPLX_0:def 7

.= e ;

||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * (NrProduct x) by A6;

hence ||.((xseq . n) - (xseq . m)).|| < e by A18, A19, XXREAL_0:2; :: thesis: verum

for n, m being Nat st n >= k & m >= k holds

||.((xseq . n) - (xseq . m)).|| < e ; :: thesis: verum

hence S

A20: for x being Element of (product X) holds S

reconsider tseq = f as Function of (product X),Y ;

A21: for u being Point of (product X)

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 (product X); :: 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 (product X) ;

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 )

thus (tseq * (reproj (i,u))) . x = lim xseq by A22, A23, FUNCT_1:13; :: thesis: verum

end;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 (product X) ;

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

thus
xseq is convergent
by A22; :: thesis: (tseq * (reproj (i,u))) . x = lim xseq
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 A23, FUNCT_1:13

.= ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x by LOPBAN10:def 13 ; :: thesis: verum

end;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 A23, FUNCT_1:13

.= ((modetrans ((vseq . n),X,Y)) * (reproj (i,u))) . x by LOPBAN10:def 13 ; :: thesis: verum

thus (tseq * (reproj (i,u))) . x = lim xseq by A22, A23, FUNCT_1:13; :: thesis: verum

now :: thesis: for i being Element of dom X

for u being Point of (product X) holds tseq * (reproj (i,u)) is LinearOperator of (X . i),Y

then reconsider tseq = tseq as MultilinearOperator of X,Y by LOPBAN10:def 6;for u being Point of (product X) holds tseq * (reproj (i,u)) is LinearOperator of (X . i),Y

let i be Element of dom X; :: thesis: for u being Point of (product X) holds tseq * (reproj (i,u)) is LinearOperator of (X . i),Y

let u be Point of (product X); :: thesis: tseq * (reproj (i,u)) is LinearOperator of (X . i),Y

set tseqiu = tseq * (reproj (i,u));

deffunc H_{1}( Nat) -> Element of K16(K17( the carrier of (X . i), the carrier of Y)) = (modetrans ((vseq . $1),X,Y)) * (reproj (i,u));

end;let u be Point of (product X); :: thesis: tseq * (reproj (i,u)) is LinearOperator of (X . i),Y

set tseqiu = tseq * (reproj (i,u));

deffunc H

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 = H_{1}(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 = H_{1}(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 = H_{1}(n) . y
and

A31: yseq is convergent and

A32: (tseq * (reproj (i,u))) . y = lim yseq by A21;

hence (tseq * (reproj (i,u))) . (x + y) = ((tseq * (reproj (i,u))) . x) + ((tseq * (reproj (i,u))) . y) by A26, A27, A29, A31, A32, NORMSP_1:25; :: thesis: verum

end;consider xseq being sequence of Y such that

A25: for n being Nat holds xseq . n = H

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 = H

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 = H

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)

then
zseq = xseq + yseq
by NORMSP_1:def 2;let n be Nat; :: thesis: zseq . n = (xseq . n) + (yseq . n)

A33: H_{1}(n) is LinearOperator of (X . i),Y
by LOPBAN10:def 6;

thus zseq . n = H_{1}(n) . (x + y)
by A28

.= (H_{1}(n) . x) + (H_{1}(n) . y)
by A33, VECTSP_1:def 20

.= (xseq . n) + (H_{1}(n) . y)
by A25

.= (xseq . n) + (yseq . n) by A30 ; :: thesis: verum

end;A33: H

thus zseq . n = H

.= (H

.= (xseq . n) + (H

.= (xseq . n) + (yseq . n) by A30 ; :: thesis: verum

hence (tseq * (reproj (i,u))) . (x + y) = ((tseq * (reproj (i,u))) . x) + ((tseq * (reproj (i,u))) . y) by A26, A27, A29, A31, A32, NORMSP_1:25; :: thesis: verum

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)

hence
tseq * (reproj (i,u)) is LinearOperator of (X . i),Y
by A24, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verumfor 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 = H_{1}(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 = H_{1}(n) . (a * x)
and

zseq is convergent and

A38: (tseq * (reproj (i,u))) . (a * x) = lim zseq by A21;

hence (tseq * (reproj (i,u))) . (a * x) = a * ((tseq * (reproj (i,u))) . x) by A35, A36, A38, NORMSP_1:28; :: thesis: verum

end;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 = H

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 = H

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)

then
zseq = a * xseq
by NORMSP_1:def 5;let n be Nat; :: thesis: zseq . n = a * (xseq . n)

A39: H_{1}(n) is LinearOperator of (X . i),Y
by LOPBAN10:def 6;

thus zseq . n = H_{1}(n) . (a * x)
by A37

.= a * (H_{1}(n) . x)
by A39, LOPBAN_1:def 5

.= a * (xseq . n) by A34 ; :: thesis: verum

end;A39: H

thus zseq . n = H

.= a * (H

.= a * (xseq . n) by A34 ; :: thesis: verum

hence (tseq * (reproj (i,u))) . (a * x) = a * ((tseq * (reproj (i,u))) . x) by A35, A36, A38, NORMSP_1:28; :: thesis: verum

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

then A45:
||.vseq.|| is convergent
by SEQ_4:41;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 A2, A40, RSSPACE3:8;

reconsider k = k as Nat ;

take k = k; :: thesis: for m being Nat st m >= k holds

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 ; :: thesis: verum

end;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 A2, A40, RSSPACE3:8;

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

hence
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 A42, A43, A44, XXREAL_0:2; :: thesis: verum

end;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 A42, A43, A44, XXREAL_0:2; :: thesis: verum

|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 ; :: thesis: verum

A46: tseq is Lipschitzian

proof

A59:
for e being Real st e > 0 holds
take
lim ||.vseq.||
; :: according to LOPBAN10:def 10 :: thesis: ( 0 <= lim ||.vseq.|| & ( for b_{1} being Element of the carrier of (product X) holds ||.(tseq . b_{1}).|| <= (lim ||.vseq.||) * (NrProduct b_{1}) ) )

_{1} being Element of the carrier of (product X) holds ||.(tseq . b_{1}).|| <= (lim ||.vseq.||) * (NrProduct b_{1}) ) )
by B39, A47, SEQ_2:17, SEQ_4:41; :: thesis: verum

end;A47: now :: thesis: for x being Point of (product X) holds ||.(tseq . x).|| <= (lim ||.vseq.||) * (NrProduct x)

let x be Point of (product X); :: thesis: ||.(tseq . x).|| <= (lim ||.vseq.||) * (NrProduct x)

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 A49, A50, LOPBAN_1:20;

A52: for m being Nat holds ||.(xseq . m).|| <= ||.(vseq . m).|| * (NrProduct x)

||.xseq.|| is convergent by A49, A50, LOPBAN_1:20;

hence ||.(tseq . x).|| <= (lim ||.vseq.||) * (NrProduct x) by A45, A51, A54, A58, SEQ_2:18; :: thesis: verum

end;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 A49, A50, LOPBAN_1:20;

A52: for m being Nat holds ||.(xseq . m).|| <= ||.(vseq . m).|| * (NrProduct x)

proof

A54:
for n being Nat holds ||.xseq.|| . n <= ((NrProduct x) (#) ||.vseq.||) . n
let m be Nat; :: thesis: ||.(xseq . m).|| <= ||.(vseq . m).|| * (NrProduct x)

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).|| * (NrProduct x) by A53, LOPBAN10:45; :: thesis: verum

end;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).|| * (NrProduct x) by A53, LOPBAN10:45; :: thesis: verum

proof

A58:
lim ((NrProduct x) (#) ||.vseq.||) = (lim ||.vseq.||) * (NrProduct x)
by B39, SEQ_2:8, SEQ_4:41;
let n be Nat; :: thesis: ||.xseq.|| . n <= ((NrProduct x) (#) ||.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).|| * (NrProduct x) by A52;

hence ||.xseq.|| . n <= ((NrProduct x) (#) ||.vseq.||) . n by A55, A56, SEQ_1:9; :: thesis: verum

end;A55: ||.xseq.|| . n = ||.(xseq . n).|| by NORMSP_0:def 4;

A56: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def 4;

||.(xseq . n).|| <= ||.(vseq . n).|| * (NrProduct x) by A52;

hence ||.xseq.|| . n <= ((NrProduct x) (#) ||.vseq.||) . n by A55, A56, SEQ_1:9; :: thesis: verum

||.xseq.|| is convergent by A49, A50, LOPBAN_1:20;

hence ||.(tseq . x).|| <= (lim ||.vseq.||) * (NrProduct x) by A45, A51, A54, A58, SEQ_2:18; :: thesis: verum

now :: thesis: for n being Nat holds ||.vseq.|| . n >= 0

hence
( 0 <= lim ||.vseq.|| & ( for blet n be Nat; :: thesis: ||.vseq.|| . n >= 0

||.(vseq . n).|| >= 0 ;

hence ||.vseq.|| . n >= 0 by NORMSP_0:def 4; :: thesis: verum

end;||.(vseq . n).|| >= 0 ;

hence ||.vseq.|| . n >= 0 by NORMSP_0:def 4; :: thesis: verum

ex k being Nat st

for n being Nat st n >= k holds

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

proof

reconsider tseq = tseq as Lipschitzian MultilinearOperator of X,Y by A46;
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 (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x) )

assume e > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

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 A2, RSSPACE3:8;

take k ; :: thesis: for n being Nat st n >= k holds

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x) ; :: thesis: verum

end;for n being Nat st n >= k holds

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x) )

assume e > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

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 A2, RSSPACE3:8;

take k ; :: thesis: for n being Nat st n >= k holds

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

now :: thesis: for n being Nat st n >= k holds

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

hence
for n being Nat st n >= k holds for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

let n be Nat; :: thesis: ( n >= k implies for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x) )

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

end;assume A61: n >= k ; :: thesis: for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

now :: thesis: for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

hence
for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)
; :: thesis: verumlet x be Point of (product X); :: thesis: ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)

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)).|| * (NrProduct x)

||.((xseq . n) - (xseq . m)).|| <= e * (NrProduct x)

end;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)).|| * (NrProduct x)

proof

A69:
for m being Nat st m >= k holds
let m, k be Nat; :: thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (NrProduct x)

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 A66, a67, a68, LOPBAN10:52;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (NrProduct x) by LOPBAN10:45; :: thesis: verum

end;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 A66, a67, a68, LOPBAN10:52;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (NrProduct x) by LOPBAN10:45; :: thesis: verum

||.((xseq . n) - (xseq . m)).|| <= e * (NrProduct x)

proof

||.((xseq . n) - (tseq . x)).|| <= e * (NrProduct x)
let m be Nat; :: thesis: ( m >= k implies ||.((xseq . n) - (xseq . m)).|| <= e * (NrProduct x) )

assume m >= k ; :: thesis: ||.((xseq . n) - (xseq . m)).|| <= e * (NrProduct x)

then A70: ||.((vseq . n) - (vseq . m)).|| < e by A60, A61;

A71: ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * (NrProduct x) by A65;

||.((vseq . n) - (vseq . m)).|| * (NrProduct x) <= e * (NrProduct x) by A70, XREAL_1:64;

hence ||.((xseq . n) - (xseq . m)).|| <= e * (NrProduct x) by A71, XXREAL_0:2; :: thesis: verum

end;assume m >= k ; :: thesis: ||.((xseq . n) - (xseq . m)).|| <= e * (NrProduct x)

then A70: ||.((vseq . n) - (vseq . m)).|| < e by A60, A61;

A71: ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * (NrProduct x) by A65;

||.((vseq . n) - (vseq . m)).|| * (NrProduct x) <= e * (NrProduct x) by A70, XREAL_1:64;

hence ||.((xseq . n) - (xseq . m)).|| <= e * (NrProduct x) by A71, XXREAL_0:2; :: thesis: verum

proof

hence
||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x)
by A62; :: thesis: verum
deffunc H_{1}( Nat) -> object = ||.((xseq . $1) - (xseq . n)).||;

consider rseq being Real_Sequence such that

A72: for m being Nat holds rseq . m = H_{1}(m)
from SEQ_1:sch 1();

A74: xseq - (xseq . n) is convergent by A63, NORMSP_1:21;

lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) by A63, A64, NORMSP_1:27;

then A75: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A73, A74, LOPBAN_1:41;

for m being Nat st m >= k holds

rseq . m <= e * (NrProduct x)

hence ||.((xseq . n) - (tseq . x)).|| <= e * (NrProduct x) by A75, NORMSP_1:7; :: thesis: verum

end;consider rseq being Real_Sequence such that

A72: for m being Nat holds rseq . m = H

now :: thesis: for x being object st x in NAT holds

rseq . x = ||.(xseq - (xseq . n)).|| . x

then A73:
rseq = ||.(xseq - (xseq . n)).||
by FUNCT_2:12;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;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

A74: xseq - (xseq . n) is convergent by A63, NORMSP_1:21;

lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) by A63, A64, NORMSP_1:27;

then A75: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A73, A74, LOPBAN_1:41;

for m being Nat st m >= k holds

rseq . m <= e * (NrProduct x)

proof

then
lim rseq <= e * (NrProduct x)
by A73, A74, LOPBAN_1:41, RSSPACE2:5;
let m be Nat; :: thesis: ( m >= k implies rseq . m <= e * (NrProduct x) )

assume A76: m >= k ; :: thesis: rseq . m <= e * (NrProduct x)

rseq . m = ||.((xseq . m) - (xseq . n)).|| by A72

.= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1:7 ;

hence rseq . m <= e * (NrProduct x) by A69, A76; :: thesis: verum

end;assume A76: m >= k ; :: thesis: rseq . m <= e * (NrProduct x)

rseq . m = ||.((xseq . m) - (xseq . n)).|| by A72

.= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1:7 ;

hence rseq . m <= e * (NrProduct x) by A69, A76; :: thesis: verum

hence ||.((xseq . n) - (tseq . x)).|| <= e * (NrProduct x) by A75, NORMSP_1:7; :: thesis: verum

for x being Point of (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x) ; :: thesis: verum

reconsider tv = tseq as Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) 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

for e being Real st e > 0 holds
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 (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x) by A59, A78;

for n being Nat st n >= k holds

||.((vseq . n) - tv).|| <= e ; :: thesis: verum

end;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 (product X) holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * (NrProduct x) by A59, A78;

now :: thesis: for n being Nat st n >= k holds

||.((vseq . n) - tv).|| <= e

hence
ex k being Nat st ||.((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);

s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;

hence ||.((vseq . n) - tv).|| <= e by A84, LOPBAN10:43; :: thesis: verum

end;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 (product X) st ( for i being Element of dom X holds ||.(t . i).|| <= 1 ) holds

||.(h1 . t).|| <= e

||.(h1 . t).|| <= e

let t be Point of (product X); :: 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 * (NrProduct t) <= e * 1 by A78, XREAL_1:64;

A83: ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| <= e * (NrProduct t) by A79, A80;

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 A82, A83, XXREAL_0:2; :: thesis: verum

end;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 * (NrProduct t) <= e * 1 by A78, XREAL_1:64;

A83: ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| <= e * (NrProduct t) by A79, A80;

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 A82, A83, XXREAL_0:2; :: thesis: verum

A84: now :: thesis: for r being Real st r in PreNorms h1 holds

r <= e

( ( for s being Real st s 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 (product X) st

( r = ||.(h1 . t).|| & ( for i being Element of dom X holds ||.(t . i).|| <= 1 ) ) ;

hence r <= e by A81; :: thesis: verum

end;assume r in PreNorms h1 ; :: thesis: r <= e

then ex t being Point of (product X) st

( r = ||.(h1 . t).|| & ( for i being Element of dom X holds ||.(t . i).|| <= 1 ) ) ;

hence r <= e by A81; :: thesis: verum

s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;

hence ||.((vseq . n) - tv).|| <= e by A84, LOPBAN10:43; :: thesis: verum

for n being Nat st n >= k holds

||.((vseq . n) - tv).|| <= e ; :: thesis: verum

ex m being Nat st

for n being Nat st n >= m holds

||.((vseq . n) - tv).|| < e

proof

hence
vseq is convergent
by NORMSP_1:def 6; :: thesis: verum
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 A77, A86;

A88: e / 2 < e by A86, XREAL_1:216;

for n being Nat st n >= m holds

||.((vseq . n) - tv).|| < e ; :: thesis: verum

end;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 A77, A86;

A88: e / 2 < e by A86, XREAL_1:216;

now :: thesis: for n being Nat st n >= m holds

||.((vseq . n) - tv).|| < e

hence
ex m being Nat st ||.((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 A88, XXREAL_0:2; :: thesis: verum

end;assume n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e

then ||.((vseq . n) - tv).|| <= e / 2 by A87;

hence ||.((vseq . n) - tv).|| < e by A88, XXREAL_0:2; :: thesis: verum

for n being Nat st n >= m holds

||.((vseq . n) - tv).|| < e ; :: thesis: verum