let E, F be RealNormSpace; :: thesis: for E1 being SubRealNormSpace of E
for f being Point of 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 st
( dom g = the carrier of E & g | the carrier of E1 = 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 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 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 st
( dom g = the carrier of E & g | the carrier of E1 = 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 st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )

let f be Point of ; :: 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 st
( dom g = the carrier of E & g | the carrier of E1 = 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 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 st
( dom g = the carrier of E & g | the carrier of E1 = 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 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 ;
then reconsider Lf = L as PartFunc of E,F by PARTFUN1:46;
A5: dom Lf = E0 by ;
consider K being Real such that
A6: ( 0 <= K & ( for x being VECTOR of E1 holds ||.(L . x).|| <= K * ) ) 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
.= xx1 - xx2 by RLVECT_1:16 ;
A12: Lf /. x1 = L . xx1 by ;
Lf /. x2 = L . xx2 by ;
then (Lf /. x1) - (Lf /. x2) = (L . xx1) + ((- 1) * (L . xx2)) by
.= (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 ;
K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by ;
hence ||.((Lf /. x1) - (Lf /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| by ; :: thesis: verum
end;
then Lf is_Lipschitzian_on E0 by ;
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 ; :: thesis: verum
end;
A30: xseq + yseq is convergent by ;
A31: lim (xseq + yseq) = x + y by ;
A32: rng (xseq + yseq) c= dom Lf by ;
A33: rng xseq c= dom Lf by ;
A34: rng yseq c= dom Lf by ;
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 ;
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
.= Lf /. ((xseq . n) + (yseq . n)) by NORMSP_1:def 2
.= L . (xn + yn) by
.= (L /. xn) + (L /. yn) by VECTSP_1:def 20
.= ((Lf /* xseq) . n) + (Lf /. (yseq . n)) by
.= ((Lf /* xseq) . n) + ((Lf /* yseq) . n) by ; :: thesis: verum
end;
A41: lim (Lf /* (xseq + yseq)) = lim ((Lf /* xseq) + (Lf /* yseq)) by
.= (lim (Lf /* xseq)) + (lim (Lf /* yseq)) by ;
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 ;
a * (xseq . n) = a * xn by NORMSP_3:28;
then a * (xseq . n) in E0 by A3;
hence y in E0 by ; :: thesis: verum
end;
A47: a * xseq is convergent by ;
A48: lim (a * xseq) = a * x by ;
A49: rng (a * xseq) c= dom Lf by ;
A50: rng xseq c= dom Lf by ;
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 ;
then reconsider xn = xseq . n as Point of E1 by ;
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
.= Lf /. (a * (xseq . n)) by NORMSP_1:def 5
.= L . (a * xn) by
.= a * (L /. xn) by LOPBAN_1:def 5
.= a * ((Lf /* xseq) . n) by ; :: thesis: verum
end;
lim (Lf /* (a * xseq)) = lim (a * (Lf /* xseq)) by
.= a * (lim (Lf /* xseq)) by ;
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 ;
reconsider Pg = Pg as Lipschitzian LinearOperator of E,F by ;
reconsider g = Pg as Point of by LOPBAN_1:def 9;
A58: dom g = the carrier of E by FUNCT_2:def 1;
A61: = upper_bound (PreNorms (modetrans (f,E1,F))) by LOPBAN_1:def 13
.= upper_bound () by LOPBAN_1:29 ;
A63: = 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 <=
proof
let t be Real; :: thesis: ( t in PreNorms L implies t <= )
assume t in PreNorms L ; :: thesis: t <=
then consider w being Point of E1 such that
A64: ( t = ||.(L . 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 ;
A68: ( not PreNorms Pg is empty & PreNorms Pg is bounded_above ) by LOPBAN_1:27;
L . w = Pg . w1 by ;
then t in PreNorms Pg by ;
hence t <= by ; :: thesis: verum
end;
then A69: ||.f.|| <= by ;
for t being Real st t in PreNorms Pg holds
t <=
proof
let t be Real; :: thesis: ( t in PreNorms Pg implies t <= )
assume t in PreNorms Pg ; :: thesis: t <=
then consider x being Point of E such that
A70: ( t = ||.(Pg . 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 ;
A73: ( ||.xseq.|| is convergent & lim ||.xseq.|| = ||.(lim xseq).|| ) by ;
A74: ||.(Lf /* xseq).|| is convergent by ;
A75: ||.f.|| (#) ||.xseq.|| is convergent by ;
for n being Nat holds ||.(Lf /* xseq).|| . n <= ( (#) ||.xseq.||) . n
proof
let n be Nat; :: thesis: ||.(Lf /* xseq).|| . n <= ( (#) ||.xseq.||) . n
A77: n in NAT by ORDINAL1:def 12;
A78: rng xseq c= dom Lf by ;
xseq . n in rng xseq by ;
then reconsider xn = xseq . n as Point of E1 by ;
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
.= ||.(L . xn).|| by ;
||.(L . xn).|| <= * ||.xn.|| by LOPBAN_1:32;
then ||.(L . xn).|| <= * ||.(xseq . n).|| by NORMSP_3:28;
then ||.(L . xn).|| <= * (||.xseq.|| . n) by NORMSP_0:def 4;
hence ||.(Lf /* xseq).|| . n <= ( (#) ||.xseq.||) . n by ; :: thesis: verum
end;
then lim ||.(Lf /* xseq).|| <= lim ( (#) ||.xseq.||) by ;
then A82: lim ||.(Lf /* xseq).|| <= * by ;
||.f.|| * <= * 1 by ;
hence t <= by ; :: thesis: verum
end;
then ||.g.|| <= by ;
hence ex g being Point of st
( dom g = the carrier of E & g | the carrier of E1 = 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 ; :: thesis: for g1, g2 being Point of st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2

thus for g1, g2 being Point of 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 ; :: 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 ;
Pg2 is_continuous_on the carrier of E by ;
hence g1 = g2 by A1, A3, A5, A15, A84, A85, Th020; :: thesis: verum
end;