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).||

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)

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

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.||

for t being Real st t in PreNorms Pg holds

t <= ||.f.||

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

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

then
Lf is_Lipschitzian_on E0
by A3, A6, FUNCT_2:def 1;
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;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

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

for x being Point of E
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

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)

.= (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;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

A30:
xseq + yseq is convergent
by A24, A25, NORMSP_1:19;
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;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

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

A41: lim (Lf /* (xseq + yseq)) =
lim ((Lf /* xseq) + (Lf /* yseq))
by B34, NORMSP_1:def 2
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;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

.= (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

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

proof

then reconsider Pg = Pg as LinearOperator of E,F by A23, LOPBAN_1:def 5, VECTSP_1:def 20;
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

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)

.= 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;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

A47:
a * xseq is convergent
by A42, NORMSP_1:22;
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;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

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

lim (Lf /* (a * xseq)) =
lim (a * (Lf /* xseq))
by B50, NORMSP_1:def 5
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;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

.= a * (lim (Lf /* xseq)) by A42, NORMSP_1:28 ;

hence Pg . (a * x) = a * (Pg . x) by A20, A42, A46, A47, A48; :: thesis: verum

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

then A69:
||.f.|| <= ||.g.||
by A61, SEQ_4:45;
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;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

for t being Real st t in PreNorms Pg holds

t <= ||.f.||

proof

then
||.g.|| <= ||.f.||
by A63, SEQ_4:45;
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

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;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

then
lim ||.(Lf /* xseq).|| <= lim (||.f.|| (#) ||.xseq.||)
by A74, A75, SEQ_2:18;
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;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

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

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;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