let E, F be RealNormSpace; :: thesis: for E1 being SubRealNormSpace of E
for f being Point of (R_NormSpace_of_BoundedLinearOperators (E1,F)) st F is complete & ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) holds
( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )
let E1 be SubRealNormSpace of E; :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators (E1,F)) st F is complete & ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) holds
( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )
let f be Point of (R_NormSpace_of_BoundedLinearOperators (E1,F)); :: thesis: ( F is complete & ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) implies ( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) ) )
assume that
A1: F is complete and
A2: ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) ; :: thesis: ( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )
consider E0 being Subset of E such that
A3: ( E0 = the carrier of E1 & E0 is dense ) by A2;
reconsider L = f as Lipschitzian LinearOperator of E1,F by LOPBAN_1:def 9;
A4: ( dom L = the carrier of E1 & rng L c= the carrier of F ) by FUNCT_2:def 1;
then L in PFuncs ( the carrier of E, the carrier of F) by A3, PARTFUN1:def 3;
then reconsider Lf = L as PartFunc of E,F by PARTFUN1:46;
A5: dom Lf = E0 by A3, FUNCT_2:def 1;
consider K being Real such that
A6: ( 0 <= K & ( for x being VECTOR of E1 holds ||.(L . x).|| <= K * ||.x.|| ) ) by LOPBAN_1:def 8;
set r = K + 1;
A7: K + 0 < K + 1 by XREAL_1:8;
for x1, x2 being Point of E st x1 in E0 & x2 in E0 holds
||.((Lf /. x1) - (Lf /. x2)).|| <= (K + 1) * ||.(x1 - x2).||

proof

let x1, x2 be Point of E; :: thesis: ( x1 in E0 & x2 in E0 implies ||.((Lf /. x1) - (Lf /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| )
assume ( x1 in E0 & x2 in E0 ) ; :: thesis: ||.((Lf /. x1) - (Lf /. x2)).|| <= (K + 1) * ||.(x1 - x2).||
then reconsider xx1 = x1, xx2 = x2 as Point of E1 by A3;
A10: (- 1) * x2 = (- 1) * xx2 by NORMSP_3:28;
A11: x1 - x2 = x1 + ((- 1) * x2) by RLVECT_1:16
.= xx1 + ((- 1) * xx2) by A10, NORMSP_3:28
.= xx1 - xx2 by RLVECT_1:16 ;
A12: Lf /. x1 = L . xx1 by A4, PARTFUN1:def 6;
Lf /. x2 = L . xx2 by A4, PARTFUN1:def 6;
then (Lf /. x1) - (Lf /. x2) = (L . xx1) + ((- 1) * (L . xx2)) by A12, RLVECT_1:16
.= (L . xx1) + (L . ((- 1) * xx2)) by LOPBAN_1:def 5
.= L . (xx1 + ((- 1) * xx2)) by VECTSP_1:def 20
.= L . (xx1 - xx2) by RLVECT_1:16 ;
then ||.((Lf /. x1) - (Lf /. x2)).|| <= K * ||.(xx1 - xx2).|| by A6;
then A14: ||.((Lf /. x1) - (Lf /. x2)).|| <= K * ||.(x1 - x2).|| by A11, NORMSP_3:28;
K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by A7, XREAL_1:64;
hence ||.((Lf /. x1) - (Lf /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| by A14, XXREAL_0:2; :: thesis: verum

end;

then Lf is_Lipschitzian_on E0 by A3, A6, FUNCT_2:def 1;
then A15: Lf is_uniformly_continuous_on E0 by NFCONT_2:9;
A16: ( ex Pg being Function of E,F st
( Pg | E0 = Lf & Pg is_uniformly_continuous_on the carrier of E & ( for x being Point of E ex seq being sequence of E st
( rng seq c= E0 & seq is convergent & lim seq = x & Lf /* seq is convergent & Pg . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & Pg . x = lim (Lf /* seq) ) ) ) & ( for Pg1, Pg2 being Function of E,F st Pg1 | E0 = Lf & Pg1 is_continuous_on the carrier of E & Pg2 | E0 = Lf & Pg2 is_continuous_on the carrier of E holds
Pg1 = Pg2 ) ) by A1, A3, A5, A15, Th020;
consider Pg being Function of E,F such that
A17: Pg | E0 = Lf and
A18: Pg is_uniformly_continuous_on the carrier of E and
A19: for x being Point of E ex seq being sequence of E st
( rng seq c= E0 & seq is convergent & lim seq = x & Lf /* seq is convergent & Pg . x = lim (Lf /* seq) ) and
A20: for x being Point of E
for seq being sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & Pg . x = lim (Lf /* seq) ) and
A21: for x being Point of E ex seq being sequence of E st
( rng seq c= E0 & seq is convergent & lim seq = x & Lf /* seq is convergent & Pg . x = lim (Lf /* seq) ) and
A22: for x being Point of E
for seq being sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & Pg . x = lim (Lf /* seq) ) by A16;
A23: for x, y being Point of E holds Pg . (x + y) = (Pg . x) + (Pg . y)

proof

let x, y be Point of E; :: thesis: Pg . (x + y) = (Pg . x) + (Pg . y)
consider xseq being sequence of E such that
A24: ( rng xseq c= E0 & xseq is convergent & lim xseq = x & Lf /* xseq is convergent & Pg . x = lim (Lf /* xseq) ) by A19;
consider yseq being sequence of E such that
A25: ( rng yseq c= E0 & yseq is convergent & lim yseq = y & Lf /* yseq is convergent & Pg . y = lim (Lf /* yseq) ) by A19;
A29: rng (xseq + yseq) c= E0

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (xseq + yseq) or y in E0 )
assume y in rng (xseq + yseq) ; :: thesis: y in E0
then consider n being Element of NAT such that
A26: y = (xseq + yseq) . n by FUNCT_2:113;
( xseq . n in rng xseq & yseq . n in rng yseq ) by FUNCT_2:4;
then reconsider xn = xseq . n, yn = yseq . n as Point of E1 by A3, A24, A25;
(xseq . n) + (yseq . n) = xn + yn by NORMSP_3:28;
then (xseq . n) + (yseq . n) in E0 by A3;
hence y in E0 by A26, NORMSP_1:def 2; :: thesis: verum

end;

A30: xseq + yseq is convergent by A24, A25, NORMSP_1:19;
A31: lim (xseq + yseq) = x + y by A24, A25, NORMSP_1:25;
A32: rng (xseq + yseq) c= dom Lf by A3, A29, FUNCT_2:def 1;
A33: rng xseq c= dom Lf by A3, A24, FUNCT_2:def 1;
A34: rng yseq c= dom Lf by A3, A25, FUNCT_2:def 1;
B34: for n being Nat holds (Lf /* (xseq + yseq)) . n = ((Lf /* xseq) . n) + ((Lf /* yseq) . n)

proof

let n be Nat; :: thesis: (Lf /* (xseq + yseq)) . n = ((Lf /* xseq) . n) + ((Lf /* yseq) . n)
A35: n in NAT by ORDINAL1:def 12;
( xseq . n in rng xseq & yseq . n in rng yseq ) by FUNCT_2:4, ORDINAL1:def 12;
then reconsider xn = xseq . n, yn = yseq . n as Point of E1 by A3, A24, A25;
A37: (xseq . n) + (yseq . n) = xn + yn by NORMSP_3:28;
then (xseq . n) + (yseq . n) in the carrier of E1 ;
then A39: (xseq . n) + (yseq . n) in dom L by FUNCT_2:def 1;
thus (Lf /* (xseq + yseq)) . n = Lf /. ((xseq + yseq) . n) by A32, A35, FUNCT_2:109
.= Lf /. ((xseq . n) + (yseq . n)) by NORMSP_1:def 2
.= L . (xn + yn) by A37, A39, PARTFUN1:def 6
.= (L /. xn) + (L /. yn) by VECTSP_1:def 20
.= ((Lf /* xseq) . n) + (Lf /. (yseq . n)) by A33, A35, FUNCT_2:109
.= ((Lf /* xseq) . n) + ((Lf /* yseq) . n) by A34, A35, FUNCT_2:109 ; :: thesis: verum

end;

A41: lim (Lf /* (xseq + yseq)) = lim ((Lf /* xseq) + (Lf /* yseq)) by B34, NORMSP_1:def 2
.= (lim (Lf /* xseq)) + (lim (Lf /* yseq)) by A24, A25, NORMSP_1:25 ;
thus Pg . (x + y) = (Pg . x) + (Pg . y) by A20, A24, A25, A29, A30, A31, A41; :: thesis: verum

end;

for x being Point of E
for a being Real holds Pg . (a * x) = a * (Pg . x)

proof

let x be Point of E; :: thesis: for a being Real holds Pg . (a * x) = a * (Pg . x)
let a be Real; :: thesis: Pg . (a * x) = a * (Pg . x)
consider xseq being sequence of E such that
A42: ( rng xseq c= E0 & xseq is convergent & lim xseq = x & Lf /* xseq is convergent & Pg . x = lim (Lf /* xseq) ) by A19;
A46: rng (a * xseq) c= E0

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (a * xseq) or y in E0 )
assume y in rng (a * xseq) ; :: thesis: y in E0
then consider n being Element of NAT such that
A43: y = (a * xseq) . n by FUNCT_2:113;
xseq . n in rng xseq by FUNCT_2:4;
then reconsider xn = xseq . n as Point of E1 by A3, A42;
a * (xseq . n) = a * xn by NORMSP_3:28;
then a * (xseq . n) in E0 by A3;
hence y in E0 by A43, NORMSP_1:def 5; :: thesis: verum

end;

A47: a * xseq is convergent by A42, NORMSP_1:22;
A48: lim (a * xseq) = a * x by A42, NORMSP_1:28;
A49: rng (a * xseq) c= dom Lf by A3, A46, FUNCT_2:def 1;
A50: rng xseq c= dom Lf by A3, A42, FUNCT_2:def 1;
B50: for n being Nat holds (Lf /* (a * xseq)) . n = a * ((Lf /* xseq) . n)

proof

let n be Nat; :: thesis: (Lf /* (a * xseq)) . n = a * ((Lf /* xseq) . n)
A51: n in NAT by ORDINAL1:def 12;
xseq . n in rng xseq by FUNCT_2:4, ORDINAL1:def 12;
then reconsider xn = xseq . n as Point of E1 by A3, A42;
A53: a * (xseq . n) = a * xn by NORMSP_3:28;
then a * (xseq . n) in the carrier of E1 ;
then A55: a * (xseq . n) in dom L by FUNCT_2:def 1;
thus (Lf /* (a * xseq)) . n = Lf /. ((a * xseq) . n) by A49, A51, FUNCT_2:109
.= Lf /. (a * (xseq . n)) by NORMSP_1:def 5
.= L . (a * xn) by A53, A55, PARTFUN1:def 6
.= a * (L /. xn) by LOPBAN_1:def 5
.= a * ((Lf /* xseq) . n) by A50, A51, FUNCT_2:109 ; :: thesis: verum

end;

lim (Lf /* (a * xseq)) = lim (a * (Lf /* xseq)) by B50, NORMSP_1:def 5
.= a * (lim (Lf /* xseq)) by A42, NORMSP_1:28 ;
hence Pg . (a * x) = a * (Pg . x) by A20, A42, A46, A47, A48; :: thesis: verum

end;

then reconsider Pg = Pg as LinearOperator of E,F by A23, LOPBAN_1:def 5, VECTSP_1:def 20;
reconsider Pg = Pg as Lipschitzian LinearOperator of E,F by A18, NFCONT_2:7, LOPBAN_7:6;
reconsider g = Pg as Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) by LOPBAN_1:def 9;
A58: dom g = the carrier of E by FUNCT_2:def 1;
A61: ||.f.|| = upper_bound (PreNorms (modetrans (f,E1,F))) by LOPBAN_1:def 13
.= upper_bound (PreNorms L) by LOPBAN_1:29 ;
A63: ||.g.|| = upper_bound (PreNorms (modetrans (g,E,F))) by LOPBAN_1:def 13
.= upper_bound (PreNorms Pg) by LOPBAN_1:29 ;
for t being Real st t in PreNorms L holds
t <= ||.g.||

proof

let t be Real; :: thesis: ( t in PreNorms L implies t <= ||.g.|| )
assume t in PreNorms L ; :: thesis: t <= ||.g.||
then consider w being Point of E1 such that
A64: ( t = ||.(L . w).|| & ||.w.|| <= 1 ) ;
A65: the carrier of E1 c= the carrier of E by DUALSP01:def 16;
w in the carrier of E1 ;
then reconsider w1 = w as Point of E by A65;
A67: ||.w1.|| <= 1 by A64, NORMSP_3:28;
A68: ( not PreNorms Pg is empty & PreNorms Pg is bounded_above ) by LOPBAN_1:27;
L . w = Pg . w1 by A3, A17, FUNCT_1:49;
then t in PreNorms Pg by A64, A67;
hence t <= ||.g.|| by A63, A68, SEQ_4:def 1; :: thesis: verum

end;

then A69: ||.f.|| <= ||.g.|| by A61, SEQ_4:45;
for t being Real st t in PreNorms Pg holds
t <= ||.f.||

proof

let t be Real; :: thesis: ( t in PreNorms Pg implies t <= ||.f.|| )
assume t in PreNorms Pg ; :: thesis: t <= ||.f.||
then consider x being Point of E such that
A70: ( t = ||.(Pg . x).|| & ||.x.|| <= 1 ) ;
consider xseq being sequence of E such that
A71: ( rng xseq c= E0 & xseq is convergent & lim xseq = x & Lf /* xseq is convergent & Pg . x = lim (Lf /* xseq) ) by A19;
A72: ||.(Pg . x).|| = lim ||.(Lf /* xseq).|| by A71, LOPBAN_1:20;
A73: ( ||.xseq.|| is convergent & lim ||.xseq.|| = ||.(lim xseq).|| ) by A71, LOPBAN_1:20;
A74: ||.(Lf /* xseq).|| is convergent by A71, NORMSP_1:23;
A75: ||.f.|| (#) ||.xseq.|| is convergent by A71, LOPBAN_1:20, SEQ_2:7;
for n being Nat holds ||.(Lf /* xseq).|| . n <= (||.f.|| (#) ||.xseq.||) . n

proof

let n be Nat; :: thesis: ||.(Lf /* xseq).|| . n <= (||.f.|| (#) ||.xseq.||) . n
A77: n in NAT by ORDINAL1:def 12;
A78: rng xseq c= dom Lf by A3, A71, FUNCT_2:def 1;
xseq . n in rng xseq by FUNCT_2:4, ORDINAL1:def 12;
then reconsider xn = xseq . n as Point of E1 by A3, A71;
A80: dom Lf = the carrier of E1 by FUNCT_2:def 1;
A81: ||.(Lf /* xseq).|| . n = ||.((Lf /* xseq) . n).|| by NORMSP_0:def 4
.= ||.(Lf /. (xseq . n)).|| by A77, A78, FUNCT_2:109
.= ||.(L . xn).|| by A80, PARTFUN1:def 6 ;
||.(L . xn).|| <= ||.f.|| * ||.xn.|| by LOPBAN_1:32;
then ||.(L . xn).|| <= ||.f.|| * ||.(xseq . n).|| by NORMSP_3:28;
then ||.(L . xn).|| <= ||.f.|| * (||.xseq.|| . n) by NORMSP_0:def 4;
hence ||.(Lf /* xseq).|| . n <= (||.f.|| (#) ||.xseq.||) . n by A81, VALUED_1:6; :: thesis: verum

end;

then lim ||.(Lf /* xseq).|| <= lim (||.f.|| (#) ||.xseq.||) by A74, A75, SEQ_2:18;
then A82: lim ||.(Lf /* xseq).|| <= ||.f.|| * ||.x.|| by A71, A73, SEQ_2:8;
||.f.|| * ||.x.|| <= ||.f.|| * 1 by A70, XREAL_1:64;
hence t <= ||.f.|| by A70, A72, A82, XXREAL_0:2; :: thesis: verum

end;

then ||.g.|| <= ||.f.|| by A63, SEQ_4:45;
hence ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) by A3, A17, A21, A22, A58, A69, XXREAL_0:1; :: thesis: for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2
thus for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 :: thesis: verum

proof

let g1, g2 be Point of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: ( g1 | the carrier of E1 = f & g2 | the carrier of E1 = f implies g1 = g2 )
assume A84: ( g1 | the carrier of E1 = f & g2 | the carrier of E1 = f ) ; :: thesis: g1 = g2
reconsider Pg1 = g1, Pg2 = g2 as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
A85: Pg1 is_continuous_on the carrier of E by LMCONT1, NFCONT_2:7;
Pg2 is_continuous_on the carrier of E by LMCONT1, NFCONT_2:7;
hence g1 = g2 by A1, A3, A5, A15, A84, A85, Th020; :: thesis: verum

end;