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

seq is convergent )

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

seq is convergent

let vseq be sequence of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: 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 Z st

( ( for n being Nat holds xseq . n = (vseq . n) . $1 ) & xseq is convergent & $2 = lim xseq );

A3: for xy being Element of [:X,Y:] ex z being Element of Z st S_{1}[xy,z]

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

reconsider tseq = f as Function of [:X,Y:],Z ;

A25: for x1, x2 being Point of X

for y being Point of Y holds tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y))

for y being Point of Y

for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))

for y1, y2 being Point of Y holds tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))

for y being Point of Y

for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))

A60: tseq is Lipschitzian

ex k being Nat st

for n being Nat st n >= k holds

for x being Point of X

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

reconsider tv = tseq as Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Def9;

A89: 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

seq is convergent )

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

seq is convergent

let vseq be sequence of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: 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 = (vseq . n) . $1 ) & xseq is convergent & $2 = lim xseq );

A3: for xy being Element of [:X,Y:] ex z being Element of Z st S

proof

consider f being Function of the carrier of [:X,Y:], the carrier of Z such that
let xy be Element of [:X,Y:]; :: thesis: ex z being Element of Z st S_{1}[xy,z]

deffunc H_{1}( Nat) -> Element of the carrier of Z = (modetrans ((vseq . $1),X,Y,Z)) . xy;

consider xseq being sequence of Z 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 = (vseq . n) . xy_{1}[xy, lim xseq]

consider x being Point of X, y being Point of Y such that

A7: xy = [x,y] by PRVECT_3:18;

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

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

end;deffunc H

consider xseq being sequence of Z such that

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

A5: for n being Nat holds xseq . n = (vseq . n) . xy

proof

take
lim xseq
; :: thesis: S
let n be Nat; :: thesis: xseq . n = (vseq . n) . xy

n in NAT by ORDINAL1:def 12;

then A6: xseq . n = (modetrans ((vseq . n),X,Y,Z)) . xy by A4;

vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

hence xseq . n = (vseq . n) . xy by A6; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

then A6: xseq . n = (modetrans ((vseq . n),X,Y,Z)) . xy by A4;

vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

hence xseq . n = (vseq . n) . xy by A6; :: thesis: verum

consider x being Point of X, y being Point of Y such that

A7: xy = [x,y] by PRVECT_3:18;

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

proof

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

reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian BilinearOperator of X,Y,Z by Def9;

A9: xseq . m = (vseq . m) . (x,y) by A5, A7;

A10: xseq . k = (vseq . k) . (x,y) by A5, A7;

(xseq . m) - (xseq . k) = h1 . (x,y) by A9, A10, Th40;

then ||.((xseq . m) - (xseq . k)).|| <= (||.((vseq . m) - (vseq . k)).|| * ||.x.||) * ||.y.|| by Th32;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||) ; :: thesis: verum

end;reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian BilinearOperator of X,Y,Z by Def9;

A9: xseq . m = (vseq . m) . (x,y) by A5, A7;

A10: xseq . k = (vseq . k) . (x,y) by A5, A7;

(xseq . m) - (xseq . k) = h1 . (x,y) by A9, A10, Th40;

then ||.((xseq . m) - (xseq . k)).|| <= (||.((vseq . m) - (vseq . k)).|| * ||.x.||) * ||.y.|| by Th32;

hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||) ; :: 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 convergent
by A1, 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 A11: 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 A11: 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: ( ( ( x = 0. X or y = 0. Y ) & ex k being Nat st

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

||.((xseq . n) - (xseq . m)).|| < e ) or ( x <> 0. X & y <> 0. Y & 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 ( x <> 0. X & y <> 0. Y & ex k being Nat st

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

||.((xseq . n) - (xseq . m)).|| < e ) )

per cases
( x = 0. X or y = 0. Y or ( x <> 0. X & y <> 0. Y ) )
;

end;

case A12:
( x = 0. X or y = 0. Y )
; :: 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

A13: xseq . m = (vseq . m) . (x,y) by A5, A7;

A14: ( vseq . m is Lipschitzian BilinearOperator of X,Y,Z & vseq . n is Lipschitzian BilinearOperator of X,Y,Z ) by Def9;

A15: ( x = 0 * x or y = 0 * y ) by A12;

then A16: (vseq . m) . (x,y) = 0 * ((vseq . m) . (x,y)) by A14, LOPBAN_8:12

.= 0. Z by RLVECT_1:10 ;

A17: xseq . n = (vseq . n) . (x,y) by A5, A7;

(vseq . n) . (x,y) = 0 * ((vseq . n) . (x,y)) by A14, A15, LOPBAN_8:12

.= 0. Z by RLVECT_1:10 ;

hence ||.((xseq . n) - (xseq . m)).|| < e by A11, A13, A16, A17; :: thesis: verum

end;assume that

n >= k and

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

A13: xseq . m = (vseq . m) . (x,y) by A5, A7;

A14: ( vseq . m is Lipschitzian BilinearOperator of X,Y,Z & vseq . n is Lipschitzian BilinearOperator of X,Y,Z ) by Def9;

A15: ( x = 0 * x or y = 0 * y ) by A12;

then A16: (vseq . m) . (x,y) = 0 * ((vseq . m) . (x,y)) by A14, LOPBAN_8:12

.= 0. Z by RLVECT_1:10 ;

A17: xseq . n = (vseq . n) . (x,y) by A5, A7;

(vseq . n) . (x,y) = 0 * ((vseq . n) . (x,y)) by A14, A15, LOPBAN_8:12

.= 0. Z by RLVECT_1:10 ;

hence ||.((xseq . n) - (xseq . m)).|| < e by A11, A13, A16, A17; :: thesis: verum

case
( x <> 0. X & y <> 0. Y )
; :: 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
( ||.x.|| <> 0 & ||.y.|| <> 0 )
by NORMSP_0:def 5;

then ( ||.x.|| > 0 & ||.y.|| > 0 ) ;

then A18: 0 < ||.x.|| * ||.y.|| by XREAL_1:129;

then consider k being Nat such that

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

||.((vseq . n) - (vseq . m)).|| < e / (||.x.|| * ||.y.||) by A2, A11, XREAL_1:139, 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 ( ||.x.|| > 0 & ||.y.|| > 0 ) ;

then A18: 0 < ||.x.|| * ||.y.|| by XREAL_1:129;

then consider k being Nat such that

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

||.((vseq . n) - (vseq . m)).|| < e / (||.x.|| * ||.y.||) by A2, A11, XREAL_1:139, 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

A20: n >= k and

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

||.((vseq . n) - (vseq . m)).|| < e / (||.x.|| * ||.y.||) by A19, A20, A21;

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

A23: (e / (||.x.|| * ||.y.||)) * (||.x.|| * ||.y.||) = (e * ((||.x.|| * ||.y.||) ")) * (||.x.|| * ||.y.||) by XCMPLX_0:def 9

.= e * (((||.x.|| * ||.y.||) ") * (||.x.|| * ||.y.||))

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

.= e ;

||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * (||.x.|| * ||.y.||) by A8;

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

end;assume that

A20: n >= k and

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

||.((vseq . n) - (vseq . m)).|| < e / (||.x.|| * ||.y.||) by A19, A20, A21;

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

A23: (e / (||.x.|| * ||.y.||)) * (||.x.|| * ||.y.||) = (e * ((||.x.|| * ||.y.||) ")) * (||.x.|| * ||.y.||) by XCMPLX_0:def 9

.= e * (((||.x.|| * ||.y.||) ") * (||.x.|| * ||.y.||))

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

.= e ;

||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * (||.x.|| * ||.y.||) by A8;

hence ||.((xseq . n) - (xseq . m)).|| < e by A22, A23, 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

A24: for z being Element of [:X,Y:] holds S

reconsider tseq = f as Function of [:X,Y:],Z ;

A25: for x1, x2 being Point of X

for y being Point of Y holds tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y))

proof

A33:
for x being Point of X
let x1, x2 be Point of X; :: thesis: for y being Point of Y holds tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y))

let y be Point of Y; :: thesis: tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y))

reconsider x1y = [x1,y] as Point of [:X,Y:] ;

reconsider x2y = [x2,y] as Point of [:X,Y:] ;

reconsider x1x2y = [(x1 + x2),y] as Point of [:X,Y:] ;

consider sqx1y being sequence of Z such that

A26: for n being Nat holds

( sqx1y . n = (vseq . n) . x1y & sqx1y is convergent & tseq . x1y = lim sqx1y ) by A24;

consider sqx2y being sequence of Z such that

A27: for n being Nat holds

( sqx2y . n = (vseq . n) . x2y & sqx2y is convergent & tseq . x2y = lim sqx2y ) by A24;

consider sqx1x2y being sequence of Z such that

A28: for n being Nat holds

( sqx1x2y . n = (vseq . n) . x1x2y & sqx1x2y is convergent & tseq . x1x2y = lim sqx1x2y ) by A24;

for n being Nat holds sqx1x2y . n = (sqx1y . n) + (sqx2y . n)

thus tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y)) by A26, A27, A28, A32, NORMSP_1:25; :: thesis: verum

end;let y be Point of Y; :: thesis: tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y))

reconsider x1y = [x1,y] as Point of [:X,Y:] ;

reconsider x2y = [x2,y] as Point of [:X,Y:] ;

reconsider x1x2y = [(x1 + x2),y] as Point of [:X,Y:] ;

consider sqx1y being sequence of Z such that

A26: for n being Nat holds

( sqx1y . n = (vseq . n) . x1y & sqx1y is convergent & tseq . x1y = lim sqx1y ) by A24;

consider sqx2y being sequence of Z such that

A27: for n being Nat holds

( sqx2y . n = (vseq . n) . x2y & sqx2y is convergent & tseq . x2y = lim sqx2y ) by A24;

consider sqx1x2y being sequence of Z such that

A28: for n being Nat holds

( sqx1x2y . n = (vseq . n) . x1x2y & sqx1x2y is convergent & tseq . x1x2y = lim sqx1x2y ) by A24;

for n being Nat holds sqx1x2y . n = (sqx1y . n) + (sqx2y . n)

proof

then A32:
sqx1x2y = sqx1y + sqx2y
by NORMSP_1:def 2;
let n be Nat; :: thesis: sqx1x2y . n = (sqx1y . n) + (sqx2y . n)

A29: vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

A30: sqx1y . n = (vseq . n) . (x1,y) by A26;

A31: sqx2y . n = (vseq . n) . (x2,y) by A27;

thus sqx1x2y . n = (vseq . n) . ((x1 + x2),y) by A28

.= (sqx1y . n) + (sqx2y . n) by A29, A30, A31, LOPBAN_8:12 ; :: thesis: verum

end;A29: vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

A30: sqx1y . n = (vseq . n) . (x1,y) by A26;

A31: sqx2y . n = (vseq . n) . (x2,y) by A27;

thus sqx1x2y . n = (vseq . n) . ((x1 + x2),y) by A28

.= (sqx1y . n) + (sqx2y . n) by A29, A30, A31, LOPBAN_8:12 ; :: thesis: verum

thus tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y)) by A26, A27, A28, A32, NORMSP_1:25; :: thesis: verum

for y being Point of Y

for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))

proof

A40:
for x being Point of X
let x be Point of X; :: thesis: for y being Point of Y

for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))

let y be Point of Y; :: thesis: for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))

let a be Real; :: thesis: tseq . ((a * x),y) = a * (tseq . (x,y))

reconsider xy = [x,y] as Point of [:X,Y:] ;

reconsider axy = [(a * x),y] as Point of [:X,Y:] ;

consider sqxy being sequence of Z such that

A34: for n being Nat holds

( sqxy . n = (vseq . n) . xy & sqxy is convergent & tseq . xy = lim sqxy ) by A24;

consider sqaxy being sequence of Z such that

A35: for n being Nat holds

( sqaxy . n = (vseq . n) . axy & sqaxy is convergent & tseq . axy = lim sqaxy ) by A24;

for n being Nat holds sqaxy . n = a * (sqxy . n)

hence tseq . ((a * x),y) = a * (tseq . (x,y)) by A34, A35, NORMSP_1:28; :: thesis: verum

end;for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))

let y be Point of Y; :: thesis: for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))

let a be Real; :: thesis: tseq . ((a * x),y) = a * (tseq . (x,y))

reconsider xy = [x,y] as Point of [:X,Y:] ;

reconsider axy = [(a * x),y] as Point of [:X,Y:] ;

consider sqxy being sequence of Z such that

A34: for n being Nat holds

( sqxy . n = (vseq . n) . xy & sqxy is convergent & tseq . xy = lim sqxy ) by A24;

consider sqaxy being sequence of Z such that

A35: for n being Nat holds

( sqaxy . n = (vseq . n) . axy & sqaxy is convergent & tseq . axy = lim sqaxy ) by A24;

for n being Nat holds sqaxy . n = a * (sqxy . n)

proof

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

A36: vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

sqaxy . n = (vseq . n) . ((a * x),y) by A35

.= a * ((vseq . n) . (x,y)) by A36, LOPBAN_8:12 ;

hence sqaxy . n = a * (sqxy . n) by A34; :: thesis: verum

end;A36: vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

sqaxy . n = (vseq . n) . ((a * x),y) by A35

.= a * ((vseq . n) . (x,y)) by A36, LOPBAN_8:12 ;

hence sqaxy . n = a * (sqxy . n) by A34; :: thesis: verum

hence tseq . ((a * x),y) = a * (tseq . (x,y)) by A34, A35, NORMSP_1:28; :: thesis: verum

for y1, y2 being Point of Y holds tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))

proof

for x being Point of X
let x be Point of X; :: thesis: for y1, y2 being Point of Y holds tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))

let y1, y2 be Point of Y; :: thesis: tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))

reconsider x1y = [x,y1] as Point of [:X,Y:] ;

reconsider x2y = [x,y2] as Point of [:X,Y:] ;

reconsider x1x2y = [x,(y1 + y2)] as Point of [:X,Y:] ;

consider sqx1y being sequence of Z such that

A41: for n being Nat holds

( sqx1y . n = (vseq . n) . x1y & sqx1y is convergent & tseq . x1y = lim sqx1y ) by A24;

consider sqx2y being sequence of Z such that

A42: for n being Nat holds

( sqx2y . n = (vseq . n) . x2y & sqx2y is convergent & tseq . x2y = lim sqx2y ) by A24;

consider sqx1x2y being sequence of Z such that

A43: for n being Nat holds

( sqx1x2y . n = (vseq . n) . x1x2y & sqx1x2y is convergent & tseq . x1x2y = lim sqx1x2y ) by A24;

for n being Nat holds sqx1x2y . n = (sqx1y . n) + (sqx2y . n)

hence tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2)) by A41, A42, A43, NORMSP_1:25; :: thesis: verum

end;let y1, y2 be Point of Y; :: thesis: tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))

reconsider x1y = [x,y1] as Point of [:X,Y:] ;

reconsider x2y = [x,y2] as Point of [:X,Y:] ;

reconsider x1x2y = [x,(y1 + y2)] as Point of [:X,Y:] ;

consider sqx1y being sequence of Z such that

A41: for n being Nat holds

( sqx1y . n = (vseq . n) . x1y & sqx1y is convergent & tseq . x1y = lim sqx1y ) by A24;

consider sqx2y being sequence of Z such that

A42: for n being Nat holds

( sqx2y . n = (vseq . n) . x2y & sqx2y is convergent & tseq . x2y = lim sqx2y ) by A24;

consider sqx1x2y being sequence of Z such that

A43: for n being Nat holds

( sqx1x2y . n = (vseq . n) . x1x2y & sqx1x2y is convergent & tseq . x1x2y = lim sqx1x2y ) by A24;

for n being Nat holds sqx1x2y . n = (sqx1y . n) + (sqx2y . n)

proof

then
sqx1x2y = sqx1y + sqx2y
by NORMSP_1:def 2;
let n be Nat; :: thesis: sqx1x2y . n = (sqx1y . n) + (sqx2y . n)

A44: vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

A45: sqx1y . n = (vseq . n) . (x,y1) by A41;

A46: sqx2y . n = (vseq . n) . (x,y2) by A42;

thus sqx1x2y . n = (vseq . n) . (x,(y1 + y2)) by A43

.= (sqx1y . n) + (sqx2y . n) by A44, A45, A46, LOPBAN_8:12 ; :: thesis: verum

end;A44: vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

A45: sqx1y . n = (vseq . n) . (x,y1) by A41;

A46: sqx2y . n = (vseq . n) . (x,y2) by A42;

thus sqx1x2y . n = (vseq . n) . (x,(y1 + y2)) by A43

.= (sqx1y . n) + (sqx2y . n) by A44, A45, A46, LOPBAN_8:12 ; :: thesis: verum

hence tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2)) by A41, A42, A43, NORMSP_1:25; :: thesis: verum

for y being Point of Y

for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))

proof

then reconsider tseq = tseq as BilinearOperator of X,Y,Z by A25, A33, A40, LOPBAN_8:12;
let x be Point of X; :: thesis: for y being Point of Y

for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))

let y be Point of Y; :: thesis: for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))

let a be Real; :: thesis: tseq . (x,(a * y)) = a * (tseq . (x,y))

reconsider xy = [x,y] as Point of [:X,Y:] ;

reconsider axy = [x,(a * y)] as Point of [:X,Y:] ;

consider sqxy being sequence of Z such that

A48: for n being Nat holds

( sqxy . n = (vseq . n) . xy & sqxy is convergent & tseq . xy = lim sqxy ) by A24;

consider sqaxy being sequence of Z such that

A49: for n being Nat holds

( sqaxy . n = (vseq . n) . axy & sqaxy is convergent & tseq . axy = lim sqaxy ) by A24;

for n being Nat holds sqaxy . n = a * (sqxy . n)

hence tseq . (x,(a * y)) = a * (tseq . (x,y)) by A48, A49, NORMSP_1:28; :: thesis: verum

end;for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))

let y be Point of Y; :: thesis: for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))

let a be Real; :: thesis: tseq . (x,(a * y)) = a * (tseq . (x,y))

reconsider xy = [x,y] as Point of [:X,Y:] ;

reconsider axy = [x,(a * y)] as Point of [:X,Y:] ;

consider sqxy being sequence of Z such that

A48: for n being Nat holds

( sqxy . n = (vseq . n) . xy & sqxy is convergent & tseq . xy = lim sqxy ) by A24;

consider sqaxy being sequence of Z such that

A49: for n being Nat holds

( sqaxy . n = (vseq . n) . axy & sqaxy is convergent & tseq . axy = lim sqaxy ) by A24;

for n being Nat holds sqaxy . n = a * (sqxy . n)

proof

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

A50: vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

sqaxy . n = (vseq . n) . (x,(a * y)) by A49

.= a * ((vseq . n) . (x,y)) by A50, LOPBAN_8:12 ;

hence sqaxy . n = a * (sqxy . n) by A48; :: thesis: verum

end;A50: vseq . n is Lipschitzian BilinearOperator of X,Y,Z by Def9;

sqaxy . n = (vseq . n) . (x,(a * y)) by A49

.= a * ((vseq . n) . (x,y)) by A50, LOPBAN_8:12 ;

hence sqaxy . n = a * (sqxy . n) by A48; :: thesis: verum

hence tseq . (x,(a * y)) = a * (tseq . (x,y)) by A48, A49, NORMSP_1:28; :: thesis: verum

B53: 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 A59:
||.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 A54: 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

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

||.((vseq . n) - (vseq . m)).|| < e by A2, A54, 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 A54: 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

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

||.((vseq . n) - (vseq . m)).|| < e by A2, A54, 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 A56: ||.((vseq . m) - (vseq . k)).|| < e by A55;

A57: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def 4;

A58: ||.(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 A56, A57, A58, XXREAL_0:2; :: thesis: verum

end;assume m >= k ; :: thesis: |.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1

then A56: ||.((vseq . m) - (vseq . k)).|| < e by A55;

A57: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def 4;

A58: ||.(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 A56, A57, A58, XXREAL_0:2; :: thesis: verum

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

A60: tseq is Lipschitzian

proof

A73:
for e being Real st e > 0 holds
take
lim ||.vseq.||
; :: according to LOPBAN_9:def 3 :: thesis: ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X

for y being VECTOR of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.|| ) )

for y being VECTOR of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.|| ) ) by B53, A61, SEQ_2:17, SEQ_4:41; :: thesis: verum

end;for y being VECTOR of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.|| ) )

A61: now :: thesis: for x being Point of X

for y being Point of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||

for y being Point of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||

let x be Point of X; :: thesis: for y being Point of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||

let y be Point of Y; :: thesis: ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||

reconsider xy = [x,y] as Point of [:X,Y:] ;

consider xyseq being sequence of Z such that

A62: for n being Nat holds xyseq . n = (vseq . n) . xy and

A63: xyseq is convergent and

A64: tseq . xy = lim xyseq by A24;

A65: ||.(tseq . xy).|| = lim ||.xyseq.|| by A63, A64, LOPBAN_1:20;

A66: for m being Nat holds ||.(xyseq . m).|| <= ||.(vseq . m).|| * (||.x.|| * ||.y.||)

||.xyseq.|| is convergent by A63, A64, LOPBAN_1:20;

hence ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.|| by A59, A65, A68, A72, SEQ_2:18; :: thesis: verum

end;let y be Point of Y; :: thesis: ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.||

reconsider xy = [x,y] as Point of [:X,Y:] ;

consider xyseq being sequence of Z such that

A62: for n being Nat holds xyseq . n = (vseq . n) . xy and

A63: xyseq is convergent and

A64: tseq . xy = lim xyseq by A24;

A65: ||.(tseq . xy).|| = lim ||.xyseq.|| by A63, A64, LOPBAN_1:20;

A66: for m being Nat holds ||.(xyseq . m).|| <= ||.(vseq . m).|| * (||.x.|| * ||.y.||)

proof

A68:
for n being Nat holds ||.xyseq.|| . n <= ((||.x.|| * ||.y.||) (#) ||.vseq.||) . n
let m be Nat; :: thesis: ||.(xyseq . m).|| <= ||.(vseq . m).|| * (||.x.|| * ||.y.||)

vseq . m is Lipschitzian BilinearOperator of X,Y,Z by Def9;

then ||.((vseq . m) . (x,y)).|| <= (||.(vseq . m).|| * ||.x.||) * ||.y.|| by Th32;

hence ||.(xyseq . m).|| <= ||.(vseq . m).|| * (||.x.|| * ||.y.||) by A62; :: thesis: verum

end;vseq . m is Lipschitzian BilinearOperator of X,Y,Z by Def9;

then ||.((vseq . m) . (x,y)).|| <= (||.(vseq . m).|| * ||.x.||) * ||.y.|| by Th32;

hence ||.(xyseq . m).|| <= ||.(vseq . m).|| * (||.x.|| * ||.y.||) by A62; :: thesis: verum

proof

A72:
lim ((||.x.|| * ||.y.||) (#) ||.vseq.||) = (lim ||.vseq.||) * (||.x.|| * ||.y.||)
by B53, SEQ_2:8, SEQ_4:41;
let n be Nat; :: thesis: ||.xyseq.|| . n <= ((||.x.|| * ||.y.||) (#) ||.vseq.||) . n

A69: ||.xyseq.|| . n = ||.(xyseq . n).|| by NORMSP_0:def 4;

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

||.(xyseq . n).|| <= ||.(vseq . n).|| * (||.x.|| * ||.y.||) by A66;

hence ||.xyseq.|| . n <= ((||.x.|| * ||.y.||) (#) ||.vseq.||) . n by A69, A70, SEQ_1:9; :: thesis: verum

end;A69: ||.xyseq.|| . n = ||.(xyseq . n).|| by NORMSP_0:def 4;

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

||.(xyseq . n).|| <= ||.(vseq . n).|| * (||.x.|| * ||.y.||) by A66;

hence ||.xyseq.|| . n <= ((||.x.|| * ||.y.||) (#) ||.vseq.||) . n by A69, A70, SEQ_1:9; :: thesis: verum

||.xyseq.|| is convergent by A63, A64, LOPBAN_1:20;

hence ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.|| by A59, A65, A68, A72, SEQ_2:18; :: thesis: verum

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

hence
( 0 <= lim ||.vseq.|| & ( for x being VECTOR of Xlet 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

for y being VECTOR of Y holds ||.(tseq . (x,y)).|| <= ((lim ||.vseq.||) * ||.x.||) * ||.y.|| ) ) by B53, A61, SEQ_2:17, SEQ_4:41; :: thesis: verum

ex k being Nat st

for n being Nat st n >= k holds

for x being Point of X

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

proof

reconsider tseq = tseq as Lipschitzian BilinearOperator of X,Y,Z by A60;
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 X

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

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

for n being Nat st n >= k holds

for x being Point of X

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

then consider k being Nat such that

A74: 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 X

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

for x being Point of X

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

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

for x being Point of X

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

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

for n being Nat st n >= k holds

for x being Point of X

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

then consider k being Nat such that

A74: 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 X

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

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

for x being Point of X

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

hence
for n being Nat st n >= k holds for x being Point of X

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

let n be Nat; :: thesis: ( n >= k implies for x being Point of X

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

assume A75: n >= k ; :: thesis: for x being Point of X

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

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

end;for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| )

assume A75: n >= k ; :: thesis: for x being Point of X

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

now :: thesis: for x being Point of X

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

hence
for x being Point of Xfor y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||

let x be Point of X; :: thesis: for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||

let y be Point of Y; :: thesis: ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||

reconsider xy = [x,y] as Point of [:X,Y:] ;

consider xyseq being sequence of Z such that

A76: for n being Nat holds xyseq . n = (vseq . n) . xy and

A77: xyseq is convergent and

A78: tseq . xy = lim xyseq by A24;

A79: for m, k being Nat holds ||.((xyseq . m) - (xyseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||)

||.((xyseq . n) - (xyseq . m)).|| <= (e * ||.x.||) * ||.y.||

end;let y be Point of Y; :: thesis: ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||

reconsider xy = [x,y] as Point of [:X,Y:] ;

consider xyseq being sequence of Z such that

A76: for n being Nat holds xyseq . n = (vseq . n) . xy and

A77: xyseq is convergent and

A78: tseq . xy = lim xyseq by A24;

A79: for m, k being Nat holds ||.((xyseq . m) - (xyseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||)

proof

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

reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian BilinearOperator of X,Y,Z by Def9;

xyseq . k = (vseq . k) . xy by A76;

then (xyseq . m) - (xyseq . k) = ((vseq . m) . (x,y)) - ((vseq . k) . (x,y)) by A76

.= h1 . (x,y) by Th40 ;

then ||.((xyseq . m) - (xyseq . k)).|| <= (||.((vseq . m) - (vseq . k)).|| * ||.x.||) * ||.y.|| by Th32;

hence ||.((xyseq . m) - (xyseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||) ; :: thesis: verum

end;reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian BilinearOperator of X,Y,Z by Def9;

xyseq . k = (vseq . k) . xy by A76;

then (xyseq . m) - (xyseq . k) = ((vseq . m) . (x,y)) - ((vseq . k) . (x,y)) by A76

.= h1 . (x,y) by Th40 ;

then ||.((xyseq . m) - (xyseq . k)).|| <= (||.((vseq . m) - (vseq . k)).|| * ||.x.||) * ||.y.|| by Th32;

hence ||.((xyseq . m) - (xyseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * (||.x.|| * ||.y.||) ; :: thesis: verum

||.((xyseq . n) - (xyseq . m)).|| <= (e * ||.x.||) * ||.y.||

proof

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

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

then A82: ||.((vseq . n) - (vseq . m)).|| < e by A74, A75;

A83: ||.((xyseq . n) - (xyseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * (||.x.|| * ||.y.||) by A79;

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

hence ||.((xyseq . n) - (xyseq . m)).|| <= (e * ||.x.||) * ||.y.|| by A83, XXREAL_0:2; :: thesis: verum

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

then A82: ||.((vseq . n) - (vseq . m)).|| < e by A74, A75;

A83: ||.((xyseq . n) - (xyseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * (||.x.|| * ||.y.||) by A79;

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

hence ||.((xyseq . n) - (xyseq . m)).|| <= (e * ||.x.||) * ||.y.|| by A83, XXREAL_0:2; :: thesis: verum

proof

hence
||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
by A76; :: thesis: verum
deffunc H_{1}( Nat) -> object = ||.((xyseq . $1) - (xyseq . n)).||;

consider rseq being Real_Sequence such that

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

A86: xyseq - (xyseq . n) is convergent by A77, NORMSP_1:21;

lim (xyseq - (xyseq . n)) = (tseq . (x,y)) - (xyseq . n) by A77, A78, NORMSP_1:27;

then A87: lim rseq = ||.((tseq . (x,y)) - (xyseq . n)).|| by A85, A86, LOPBAN_1:41;

for m being Nat st m >= k holds

rseq . m <= (e * ||.x.||) * ||.y.||

hence ||.((xyseq . n) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| by A87, NORMSP_1:7; :: thesis: verum

end;consider rseq being Real_Sequence such that

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

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

rseq . i = ||.(xyseq - (xyseq . n)).|| . i

then A85:
rseq = ||.(xyseq - (xyseq . n)).||
by FUNCT_2:12;rseq . i = ||.(xyseq - (xyseq . n)).|| . i

let i be object ; :: thesis: ( i in NAT implies rseq . i = ||.(xyseq - (xyseq . n)).|| . i )

assume i in NAT ; :: thesis: rseq . i = ||.(xyseq - (xyseq . n)).|| . i

then reconsider k = i as Nat ;

thus rseq . i = ||.((xyseq . k) - (xyseq . n)).|| by A84

.= ||.((xyseq - (xyseq . n)) . k).|| by NORMSP_1:def 4

.= ||.(xyseq - (xyseq . n)).|| . i by NORMSP_0:def 4 ; :: thesis: verum

end;assume i in NAT ; :: thesis: rseq . i = ||.(xyseq - (xyseq . n)).|| . i

then reconsider k = i as Nat ;

thus rseq . i = ||.((xyseq . k) - (xyseq . n)).|| by A84

.= ||.((xyseq - (xyseq . n)) . k).|| by NORMSP_1:def 4

.= ||.(xyseq - (xyseq . n)).|| . i by NORMSP_0:def 4 ; :: thesis: verum

A86: xyseq - (xyseq . n) is convergent by A77, NORMSP_1:21;

lim (xyseq - (xyseq . n)) = (tseq . (x,y)) - (xyseq . n) by A77, A78, NORMSP_1:27;

then A87: lim rseq = ||.((tseq . (x,y)) - (xyseq . n)).|| by A85, A86, LOPBAN_1:41;

for m being Nat st m >= k holds

rseq . m <= (e * ||.x.||) * ||.y.||

proof

then
lim rseq <= (e * ||.x.||) * ||.y.||
by A85, A86, LOPBAN_1:41, Lm3;
let m be Nat; :: thesis: ( m >= k implies rseq . m <= (e * ||.x.||) * ||.y.|| )

assume A88: m >= k ; :: thesis: rseq . m <= (e * ||.x.||) * ||.y.||

rseq . m = ||.((xyseq . m) - (xyseq . n)).|| by A84

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

hence rseq . m <= (e * ||.x.||) * ||.y.|| by A81, A88; :: thesis: verum

end;assume A88: m >= k ; :: thesis: rseq . m <= (e * ||.x.||) * ||.y.||

rseq . m = ||.((xyseq . m) - (xyseq . n)).|| by A84

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

hence rseq . m <= (e * ||.x.||) * ||.y.|| by A81, A88; :: thesis: verum

hence ||.((xyseq . n) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| by A87, NORMSP_1:7; :: thesis: verum

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

for x being Point of X

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

reconsider tv = tseq as Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Def9;

A89: 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 A90: 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

A91: for n being Nat st n >= k holds

for x being Point of X

for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| by A73, A90;

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 A90: 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

A91: for n being Nat st n >= k holds

for x being Point of X

for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| by A73, A90;

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 A92: n >= k ; :: thesis: ||.((vseq . n) - tv).|| <= e

reconsider h1 = (vseq . n) - tv as Lipschitzian BilinearOperator of X,Y,Z by Def9;

set f1 = vseq . n;

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

hence ||.((vseq . n) - tv).|| <= e by A96, Th30; :: thesis: verum

end;let n be Nat; :: thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )

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

reconsider h1 = (vseq . n) - tv as Lipschitzian BilinearOperator of X,Y,Z by Def9;

set f1 = vseq . n;

A93: now :: thesis: for t being Point of X

for s being Point of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

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

for s being Point of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

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

let t be Point of X; :: thesis: for s being Point of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

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

let s be Point of Y; :: thesis: ( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(h1 . (t,s)).|| <= e )

assume ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ; :: thesis: ||.(h1 . (t,s)).|| <= e

then ||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66;

then A94: e * (||.t.|| * ||.s.||) <= e * 1 by A90, XREAL_1:64;

A95: ||.(((vseq . n) . (t,s)) - (tseq . (t,s))).|| <= (e * ||.t.||) * ||.s.|| by A91, A92;

||.(h1 . (t,s)).|| = ||.(((vseq . n) . (t,s)) - (tseq . (t,s))).|| by Th40;

hence ||.(h1 . (t,s)).|| <= e by A94, A95, XXREAL_0:2; :: thesis: verum

end;||.(h1 . (t,s)).|| <= e

let s be Point of Y; :: thesis: ( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(h1 . (t,s)).|| <= e )

assume ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ; :: thesis: ||.(h1 . (t,s)).|| <= e

then ||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66;

then A94: e * (||.t.|| * ||.s.||) <= e * 1 by A90, XREAL_1:64;

A95: ||.(((vseq . n) . (t,s)) - (tseq . (t,s))).|| <= (e * ||.t.||) * ||.s.|| by A91, A92;

||.(h1 . (t,s)).|| = ||.(((vseq . n) . (t,s)) - (tseq . (t,s))).|| by Th40;

hence ||.(h1 . (t,s)).|| <= e by A94, A95, XXREAL_0:2; :: thesis: verum

A96: 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 VECTOR of X ex s being VECTOR of Y st

( r = ||.(h1 . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

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

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

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(h1 . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

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

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

hence ||.((vseq . n) - tv).|| <= e by A96, Th30; :: 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 A98: 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

A99: for n being Nat st n >= m holds

||.((vseq . n) - tv).|| <= e / 2 by A89, A98, XREAL_1:215;

A100: e / 2 < e by A98, 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 A98: 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

A99: for n being Nat st n >= m holds

||.((vseq . n) - tv).|| <= e / 2 by A89, A98, XREAL_1:215;

A100: e / 2 < e by A98, 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 A99;

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

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

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

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

for n being Nat st n >= m holds

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