let X be RealBanachSpace; :: thesis: for Y being RealNormSpace
for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
let Y be RealNormSpace; :: thesis: for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
let T be Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) ) implies ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) ) )
assume A1: for x being Point of X ex KTx being Real st
( 0 <= KTx & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= KTx ) ) ; :: thesis: ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
per cases ( T <> {} or T = {} ) ;
suppose A2: T <> {} ; :: thesis: ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
deffunc H1( Point of X, Real) -> Subset of X = Ball ($1,$2);
defpred S1[ Point of X, set ] means $2 = { ||.(f . $1).|| where f is Lipschitzian LinearOperator of X,Y : f in T } ;
A3: for x being Point of X ex y being Element of bool REAL st S1[x,y]
proof
let x be Point of X; :: thesis: ex y being Element of bool REAL st S1[x,y]
take y = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T } ; :: thesis: ( y is Element of bool REAL & S1[x,y] )
now :: thesis: for z being object st z in y holds
z in REAL
let z be object ; :: thesis: ( z in y implies z in REAL )
assume z in y ; :: thesis: z in REAL
then ex f being Lipschitzian LinearOperator of X,Y st
( z = ||.(f . x).|| & f in T ) ;
hence z in REAL ; :: thesis: verum
end;
hence ( y is Element of bool REAL & S1[x,y] ) by TARSKI:def 3; :: thesis: verum
end;
ex Ta being Function of the carrier of X,(bool REAL) st
for x being Element of X holds S1[x,Ta . x] from FUNCT_2:sch 3(A3);
then consider Ta being Function of X,(bool REAL) such that
A4: for x being Point of X holds Ta . x = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T } ;
defpred S2[ Nat, set ] means $2 = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= $1 ) } ;
A5: for n being Element of NAT ex y being Element of bool the carrier of X st S2[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of bool the carrier of X st S2[n,y]
take y = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) } ; :: thesis: ( y is Element of bool the carrier of X & S2[n,y] )
now :: thesis: for z being object st z in y holds
z in the carrier of X
let z be object ; :: thesis: ( z in y implies z in the carrier of X )
assume z in y ; :: thesis: z in the carrier of X
then ex x being Point of X st
( z = x & Ta . x is bounded_above & upper_bound (Ta . x) <= n ) ;
hence z in the carrier of X ; :: thesis: verum
end;
hence ( y is Element of bool the carrier of X & S2[n,y] ) by TARSKI:def 3; :: thesis: verum
end;
ex Xn being sequence of (bool the carrier of X) st
for n being Element of NAT holds S2[n,Xn . n] from FUNCT_2:sch 3(A5);
then consider Xn being sequence of (bool the carrier of X) such that
A6: for n being Element of NAT holds Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) } ;
reconsider Xn = Xn as SetSequence of X ;
A7: the carrier of X c= union (rng Xn)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of X or x in union (rng Xn) )
assume x in the carrier of X ; :: thesis: x in union (rng Xn)
then reconsider x1 = x as Point of X ;
consider KTx1 being Real such that
0 <= KTx1 and
A8: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x1).|| <= KTx1 by A1;
A9: Ta . x1 = { ||.(f . x1).|| where f is Lipschitzian LinearOperator of X,Y : f in T } by A4;
A10: for p being Real st p in Ta . x1 holds
p <= KTx1
proof
let p be Real; :: thesis: ( p in Ta . x1 implies p <= KTx1 )
assume p in Ta . x1 ; :: thesis: p <= KTx1
then ex f being Lipschitzian LinearOperator of X,Y st
( p = ||.(f . x1).|| & f in T ) by A9;
hence p <= KTx1 by A8; :: thesis: verum
end;
KTx1 is UpperBound of Ta . x1
proof
let p be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not p in Ta . x1 or p <= KTx1 )
assume p in Ta . x1 ; :: thesis: p <= KTx1
then ex f being Lipschitzian LinearOperator of X,Y st
( p = ||.(f . x1).|| & f in T ) by A9;
hence p <= KTx1 by A8; :: thesis: verum
end;
then A11: Ta . x1 is bounded_above ;
consider n being Nat such that
A12: KTx1 < n by SEQ_4:3;
A13: n in NAT by ORDINAL1:def 12;
consider f being object such that
A14: f in T by A2, XBOOLE_0:def 1;
reconsider f = f as Lipschitzian LinearOperator of X,Y by A14, LOPBAN_1:def 9;
||.(f . x1).|| in Ta . x by A9, A14;
then upper_bound (Ta . x1) <= KTx1 by A10, SEQ_4:45;
then upper_bound (Ta . x1) <= n by A12, XXREAL_0:2;
then x1 in { z1 where z1 is Point of X : ( Ta . z1 is bounded_above & upper_bound (Ta . z1) <= n ) } by A11;
then x1 in Xn . n by A6, A13;
then x1 in Union Xn by PROB_1:12;
hence x in union (rng Xn) ; :: thesis: verum
end;
A15: for x being Point of X holds not Ta . x is empty
proof
let x be Point of X; :: thesis: not Ta . x is empty
consider f0 being object such that
A16: f0 in T by A2, XBOOLE_0:def 1;
reconsider f0 = f0 as Lipschitzian LinearOperator of X,Y by A16, LOPBAN_1:def 9;
Ta . x = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T } by A4;
then ||.(f0 . x).|| in Ta . x by A16;
hence not Ta . x is empty ; :: thesis: verum
end;
A17: for n being Nat holds Xn . n is closed
proof
let n be Nat; :: thesis: Xn . n is closed
A18: n in NAT by ORDINAL1:def 12;
for s1 being sequence of X st rng s1 c= Xn . n & s1 is convergent holds
lim s1 in Xn . n
proof
let s1 be sequence of X; :: thesis: ( rng s1 c= Xn . n & s1 is convergent implies lim s1 in Xn . n )
assume that
A19: rng s1 c= Xn . n and
A20: s1 is convergent ; :: thesis: lim s1 in Xn . n
A21: Ta . (lim s1) = { ||.(f . (lim s1)).|| where f is Lipschitzian LinearOperator of X,Y : f in T } by A4;
A22: for y being Real st y in Ta . (lim s1) holds
y <= n
proof
let y be Real; :: thesis: ( y in Ta . (lim s1) implies y <= n )
assume y in Ta . (lim s1) ; :: thesis: y <= n
then consider f being Lipschitzian LinearOperator of X,Y such that
A23: y = ||.(f . (lim s1)).|| and
A24: f in T by A21;
A25: f is_continuous_in lim s1 by Th4;
A26: dom f = the carrier of X by FUNCT_2:def 1;
then A27: rng s1 c= dom f by A19, XBOOLE_1:1;
then A28: f /* s1 is convergent by A20, A25, NFCONT_1:def 5;
for k being Nat holds ||.(f /* s1).|| . k <= n
proof
let k be Nat; :: thesis: ||.(f /* s1).|| . k <= n
A29: k in NAT by ORDINAL1:def 12;
||.(f /* s1).|| . k = ||.((f /* s1) . k).|| by NORMSP_0:def 4;
then A30: ||.(f /* s1).|| . k = ||.(f /. (s1 . k)).|| by A19, A26, FUNCT_2:109, A29, XBOOLE_1:1;
dom s1 = NAT by FUNCT_2:def 1;
then s1 . k in rng s1 by FUNCT_1:3, A29;
then s1 . k in Xn . n by A19;
then s1 . k in { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) } by A6, A18;
then consider x being Point of X such that
A31: x = s1 . k and
A32: Ta . x is bounded_above and
A33: upper_bound (Ta . x) <= n ;
Ta . x = { ||.(g . x).|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4;
then ||.(f . (s1 . k)).|| in Ta . (s1 . k) by A24, A31;
then ||.(f . (s1 . k)).|| <= upper_bound (Ta . (s1 . k)) by A31, A32, SEQ_4:def 1;
hence ||.(f /* s1).|| . k <= n by A30, A31, A33, XXREAL_0:2; :: thesis: verum
end;
then A34: for i being Nat st 0 <= i holds
||.(f /* s1).|| . i <= n ;
f /. (lim s1) = lim (f /* s1) by A20, A25, A27, NFCONT_1:def 5;
then lim ||.(f /* s1).|| = ||.(f /. (lim s1)).|| by A28, LOPBAN_1:20;
hence y <= n by A23, A28, A34, NORMSP_1:23, RSSPACE2:5; :: thesis: verum
end;
then for y being ExtReal st y in Ta . (lim s1) holds
y <= n ;
then A35: n is UpperBound of Ta . (lim s1) by XXREAL_2:def 1;
not Ta . (lim s1) is empty by A15;
then A36: upper_bound (Ta . (lim s1)) <= n by A22, SEQ_4:45;
A37: Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) } by A6, A18;
Ta . (lim s1) is bounded_above by A35;
hence lim s1 in Xn . n by A36, A37; :: thesis: verum
end;
hence Xn . n is closed by NFCONT_1:def 3; :: thesis: verum
end;
consider f being object such that
A38: f in T by A2, XBOOLE_0:def 1;
reconsider f = f as Lipschitzian LinearOperator of X,Y by A38, LOPBAN_1:def 9;
union (rng Xn) is Subset of X by PROB_1:11;
then union (rng Xn) = the carrier of X by A7, XBOOLE_0:def 10;
then consider n0 being Nat, r being Real, x0 being Point of X such that
A39: 0 < r and
A40: H1(x0,r) c= Xn . n0 by A17, Th3;
A41: n0 in NAT by ORDINAL1:def 12;
||.(x0 - x0).|| = ||.(0. X).|| by RLVECT_1:5;
then x0 in H1(x0,r) by A39;
then x0 in Xn . n0 by A40;
then x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) } by A6, A41;
then consider xx1 being Point of X such that
A42: xx1 = x0 and
A43: Ta . xx1 is bounded_above and
upper_bound (Ta . xx1) <= n0 ;
Ta . xx1 = { ||.(g . xx1).|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4;
then ||.(f . x0).|| in Ta . x0 by A42, A38;
then ||.(f . x0).|| <= upper_bound (Ta . x0) by A42, A43, SEQ_4:def 1;
then A44: 0 <= upper_bound (Ta . x0) ;
A45: for x being Point of X st x <> 0. X holds
((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r)
proof
let x be Point of X; :: thesis: ( x <> 0. X implies ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) )
reconsider x1 = (||.x.|| ") * x as Point of X ;
A46: ||.((r / 2) * x1).|| = |.(r / 2).| * ||.x1.|| by NORMSP_1:def 1;
assume x <> 0. X ; :: thesis: ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r)
then A47: ||.x.|| <> 0 by NORMSP_0:def 5;
||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / (2 * ||.x.||)) * x) + (x0 + (- x0))).|| by RLVECT_1:def 3;
then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / (2 * ||.x.||)) * x) + (0. X)).|| by RLVECT_1:5;
then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / (2 * ||.x.||)) * x).|| by RLVECT_1:def 4;
then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / 2) / ||.x.||) * x).|| by XCMPLX_1:78;
then A48: ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / 2) * x1).|| by RLVECT_1:def 7;
A49: |.(||.x.|| ").| = ||.x.|| " by ABSVALUE:def 1;
||.x1.|| = |.(||.x.|| ").| * ||.x.|| by NORMSP_1:def 1;
then ||.x1.|| = 1 by A47, A49, XCMPLX_0:def 7;
then ||.((r / 2) * x1).|| = r / 2 by A39, A46, ABSVALUE:def 1;
then A50: ||.(x0 - (((r / (2 * ||.x.||)) * x) + x0)).|| = r / 2 by A48, NORMSP_1:7;
r / 2 < r by A39, XREAL_1:216;
hence ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) by A50; :: thesis: verum
end;
set M = upper_bound (Ta . x0);
take KT = (2 * ((upper_bound (Ta . x0)) + n0)) / r; :: thesis: ( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= KT ) )
A51: for f being Lipschitzian LinearOperator of X,Y st f in T holds
for x being Point of X st x in H1(x0,r) holds
||.(f . x).|| <= n0
proof
let f be Lipschitzian LinearOperator of X,Y; :: thesis: ( f in T implies for x being Point of X st x in H1(x0,r) holds
||.(f . x).|| <= n0 )
assume A52: f in T ; :: thesis: for x being Point of X st x in H1(x0,r) holds
||.(f . x).|| <= n0
A53: n0 in NAT by ORDINAL1:def 12;
let x be Point of X; :: thesis: ( x in H1(x0,r) implies ||.(f . x).|| <= n0 )
assume x in H1(x0,r) ; :: thesis: ||.(f . x).|| <= n0
then x in Xn . n0 by A40;
then x in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) } by A6, A53;
then consider x1 being Point of X such that
A54: x1 = x and
A55: Ta . x1 is bounded_above and
A56: upper_bound (Ta . x1) <= n0 ;
Ta . x1 = { ||.(g . x1).|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4;
then ||.(f . x).|| in Ta . x by A52, A54;
then ||.(f . x).|| <= upper_bound (Ta . x) by A54, A55, SEQ_4:def 1;
hence ||.(f . x).|| <= n0 by A54, A56, XXREAL_0:2; :: thesis: verum
end;
A57: now :: thesis: for f being Lipschitzian LinearOperator of X,Y st f in T holds
for k being Real st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT
let f be Lipschitzian LinearOperator of X,Y; :: thesis: ( f in T implies for k being Real st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT )
assume A58: f in T ; :: thesis: for k being Real st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT
A59: for x being Point of X st x <> 0. X holds
||.(f . x).|| <= KT * ||.x.||
proof
A60: n0 in NAT by ORDINAL1:def 12;
||.(x0 - x0).|| = ||.(0. X).|| by RLVECT_1:5;
then x0 in H1(x0,r) by A39;
then x0 in Xn . n0 by A40;
then A61: x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) } by A6, A60;
set nr3 = ||.(f . x0).||;
let x be Point of X; :: thesis: ( x <> 0. X implies ||.(f . x).|| <= KT * ||.x.|| )
set nrp1 = r / (2 * ||.x.||);
set nrp2 = (2 * ||.x.||) / r;
set nr1 = ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).||;
set nr2 = ||.(f . ((r / (2 * ||.x.||)) * x)).||;
||.(- (f . x0)).|| = ||.(f . x0).|| by NORMSP_1:2;
then A62: ||.(f . ((r / (2 * ||.x.||)) * x)).|| - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) - (- (f . x0))).|| by NORMSP_1:8;
assume A63: x <> 0. X ; :: thesis: ||.(f . x).|| <= KT * ||.x.||
then A64: ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| <= n0 by A51, A45, A58;
consider x1 being Point of X such that
A65: x1 = x0 and
A66: Ta . x1 is bounded_above and
upper_bound (Ta . x1) <= n0 by A61;
Ta . x1 = { ||.(g . x1).|| where g is Lipschitzian LinearOperator of X,Y : g in T } by A4;
then ||.(f . x0).|| in Ta . x0 by A58, A65;
then ||.(f . x0).|| <= upper_bound (Ta . x0) by A65, A66, SEQ_4:def 1;
then A67: ((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| by XREAL_1:10;
||.x.|| <> 0 by A63, NORMSP_0:def 5;
then A68: ||.x.|| > 0 ;
||.(f . ((r / (2 * ||.x.||)) * x)).|| = ||.((r / (2 * ||.x.||)) * (f . x)).|| by LOPBAN_1:def 5;
then ||.(f . ((r / (2 * ||.x.||)) * x)).|| = |.(r / (2 * ||.x.||)).| * ||.(f . x).|| by NORMSP_1:def 1;
then ||.(f . ((r / (2 * ||.x.||)) * x)).|| = (r / (2 * ||.x.||)) * ||.(f . x).|| by A39, ABSVALUE:def 1;
then ( ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| = ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| & ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| ) by A62, RLVECT_1:17, VECTSP_1:def 20;
then ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= n0 by A64, XXREAL_0:2;
then ((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= n0 by A67, XXREAL_0:2;
then (((r / (2 * ||.x.||)) * ||.(f . x).||) + (- (upper_bound (Ta . x0)))) + (upper_bound (Ta . x0)) <= n0 + (upper_bound (Ta . x0)) by XREAL_1:6;
then ((2 * ||.x.||) / r) * ((r / (2 * ||.x.||)) * ||.(f . x).||) <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0))) by A39, XREAL_1:64;
then A69: ((r / (2 * ||.x.||)) * ((2 * ||.x.||) / r)) * ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0))) ;
2 * ||.x.|| > 0 by A68, XREAL_1:129;
then 1 * ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0))) by A39, A69, XCMPLX_1:112;
hence ||.(f . x).|| <= KT * ||.x.|| ; :: thesis: verum
end;
A70: for x being Point of X holds ||.(f . x).|| <= KT * ||.x.||
proof
let x be Point of X; :: thesis: ||.(f . x).|| <= KT * ||.x.||
now :: thesis: ( x = 0. X implies ||.(f . x).|| <= KT * ||.x.|| )
assume A71: x = 0. X ; :: thesis: ||.(f . x).|| <= KT * ||.x.||
then f . x = f . (0 * (0. X)) by RLVECT_1:10;
then f . x = 0 * (f . (0. X)) by LOPBAN_1:def 5;
then A72: f . x = 0. Y by RLVECT_1:10;
||.x.|| = 0 by A71;
hence ||.(f . x).|| <= KT * ||.x.|| by A72; :: thesis: verum
end;
hence ||.(f . x).|| <= KT * ||.x.|| by A59; :: thesis: verum
end;
thus for k being Real st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT :: thesis: verum
proof
let k be Real; :: thesis: ( k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } implies k <= KT )
assume k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } ; :: thesis: k <= KT
then consider x being Point of X such that
A73: ( k = ||.(f . x).|| & ||.x.|| <= 1 ) ;
( k <= KT * ||.x.|| & KT * ||.x.|| <= KT ) by A39, A44, A70, A73, XREAL_1:153;
hence k <= KT by XXREAL_0:2; :: thesis: verum
end;
end;
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= KT
proof
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( f in T implies ||.f.|| <= KT )
reconsider f1 = f as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
assume f in T ; :: thesis: ||.f.|| <= KT
then A74: for k being Real st k in PreNorms f1 holds
k <= KT by A57;
||.f.|| = upper_bound (PreNorms f1) by LOPBAN_1:30;
hence ||.f.|| <= KT by A74, SEQ_4:45; :: thesis: verum
end;
hence ( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= KT ) ) by A39, A44; :: thesis: verum
end;
suppose A75: T = {} ; :: thesis: ex L being Real st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
take 0 ; :: thesis: ( 0 <= 0 & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= 0 ) )
thus ( 0 <= 0 & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= 0 ) ) by A75; :: thesis: verum
end;
end;