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 S1[ 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 S1[xy,z]
proof
let xy be Element of [:X,Y:]; :: thesis: ex z being Element of Z st S1[xy,z]
deffunc H1( 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 = H1(n) from FUNCT_2:sch 4();
 A5: for n being Nat holds xseq . n = (vseq . n) . xy
proof
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;
take lim xseq ; :: thesis: S1[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.||)
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;
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 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 ) )
per cases ( x = 0. X or y = 0. Y or ( x <> 0. X & y <> 0. Y ) ) ;
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
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
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;
end;
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
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
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;
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 convergent by A1, RSSPACE3:8;
hence S1[xy, lim xseq] by A5; :: thesis: verum
end;
consider f being Function of the carrier of [:X,Y:], the carrier of Z such that
A24: for z being Element of [:X,Y:] holds S1[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))
proof
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)
proof
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;
then A32: sqx1x2y = sqx1y + sqx2y by NORMSP_1:def 2;
thus tseq . ((x1 + x2),y) = (tseq . (x1,y)) + (tseq . (x2,y)) by A26, A27, A28, A32, NORMSP_1:25; :: thesis: verum
end;
A33: for x being Point of X
for y being Point of Y
for a being Real holds tseq . ((a * x),y) = a * (tseq . (x,y))
proof
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)
proof
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;
then sqaxy = a * sqxy by NORMSP_1:def 5;
hence tseq . ((a * x),y) = a * (tseq . (x,y)) by A34, A35, NORMSP_1:28; :: thesis: verum
end;
A40: for x being Point of X
for y1, y2 being Point of Y holds tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2))
proof
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)
proof
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;
then sqx1x2y = sqx1y + sqx2y by NORMSP_1:def 2;
hence tseq . (x,(y1 + y2)) = (tseq . (x,y1)) + (tseq . (x,y2)) by A41, A42, A43, NORMSP_1:25; :: thesis: verum
end;
for x being Point of X
for y being Point of Y
for a being Real holds tseq . (x,(a * y)) = a * (tseq . (x,y))
proof
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)
proof
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;
then sqaxy = a * sqxy by NORMSP_1:def 5;
hence tseq . (x,(a * y)) = a * (tseq . (x,y)) by A48, A49, NORMSP_1:28; :: thesis: verum
end;
then reconsider tseq = tseq as BilinearOperator of X,Y,Z by A25, A33, A40, LOPBAN_8:12;
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
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
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 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;
hence for m being Nat st m >= k holds
|.((||.vseq.|| . m) - (||.vseq.|| . k)).| < e1 ; :: thesis: verum
end;
then A59: ||.vseq.|| is convergent by SEQ_4:41;
A60: tseq is Lipschitzian
proof
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.|| ) )
A61: now :: thesis: for x being Point of X
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.||)
proof
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;
A68: for n being Nat holds ||.xyseq.|| . n <= ((||.x.|| * ||.y.||) (#) ||.vseq.||) . n
proof
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;
A72: lim ((||.x.|| * ||.y.||) (#) ||.vseq.||) = (lim ||.vseq.||) * (||.x.|| * ||.y.||) by B53, SEQ_2:8, SEQ_4:41;
||.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;
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 x being VECTOR of X
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;
A73: 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 X
for y being Point of Y holds ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
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 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.||
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.||
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.||
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.||)
proof
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;
A81: for m being Nat st m >= k holds
||.((xyseq . n) - (xyseq . m)).|| <= (e * ||.x.||) * ||.y.||
proof
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;
||.((xyseq . n) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.||
proof
deffunc H1( Nat) -> object = ||.((xyseq . $1) - (xyseq . n)).||;
consider rseq being Real_Sequence such that
A84: for m being Nat holds rseq . m = H1(m) from SEQ_1:sch 1();
now :: thesis: for i being object st i in NAT holds
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;
then A85: rseq = ||.(xyseq - (xyseq . n)).|| by FUNCT_2:12;
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
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;
then lim rseq <= (e * ||.x.||) * ||.y.|| by A85, A86, LOPBAN_1:41, Lm3;
hence ||.((xyseq . n) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| by A87, NORMSP_1:7; :: thesis: verum
end;
hence ||.(((vseq . n) . (x,y)) - (tseq . (x,y))).|| <= (e * ||.x.||) * ||.y.|| by A76; :: thesis: verum
end;
hence 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;
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.|| ; :: thesis: verum
end;
reconsider tseq = tseq as Lipschitzian BilinearOperator of X,Y,Z by A60;
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
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;
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 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
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;
A96: 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 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;
( ( 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 A96, Th30; :: 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 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
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;
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