let E, F be RealNormSpace; :: thesis: for E1 being Subset of E
for f being PartFunc of E,F st E1 is dense & F is complete & dom f = E1 & f is_uniformly_continuous_on E1 holds
( ex g being Function of E,F st
( g | E1 = f & g is_uniformly_continuous_on the carrier of E & ( for x being Point of E ex seq being sequence of E st
( rng seq c= E1 & seq is convergent & lim seq = x & f /* seq is convergent & g . x = lim (f /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds
( f /* seq is convergent & g . x = lim (f /* seq) ) ) ) & ( for g1, g2 being Function of E,F st g1 | E1 = f & g1 is_continuous_on the carrier of E & g2 | E1 = f & g2 is_continuous_on the carrier of E holds
g1 = g2 ) )
let E1 be Subset of E; :: thesis: for f being PartFunc of E,F st E1 is dense & F is complete & dom f = E1 & f is_uniformly_continuous_on E1 holds
( ex g being Function of E,F st
( g | E1 = f & g is_uniformly_continuous_on the carrier of E & ( for x being Point of E ex seq being sequence of E st
( rng seq c= E1 & seq is convergent & lim seq = x & f /* seq is convergent & g . x = lim (f /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds
( f /* seq is convergent & g . x = lim (f /* seq) ) ) ) & ( for g1, g2 being Function of E,F st g1 | E1 = f & g1 is_continuous_on the carrier of E & g2 | E1 = f & g2 is_continuous_on the carrier of E holds
g1 = g2 ) )
let f be PartFunc of E,F; :: thesis: ( E1 is dense & F is complete & dom f = E1 & f is_uniformly_continuous_on E1 implies ( ex g being Function of E,F st
( g | E1 = f & g is_uniformly_continuous_on the carrier of E & ( for x being Point of E ex seq being sequence of E st
( rng seq c= E1 & seq is convergent & lim seq = x & f /* seq is convergent & g . x = lim (f /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds
( f /* seq is convergent & g . x = lim (f /* seq) ) ) ) & ( for g1, g2 being Function of E,F st g1 | E1 = f & g1 is_continuous_on the carrier of E & g2 | E1 = f & g2 is_continuous_on the carrier of E holds
g1 = g2 ) ) )
assume that
A1: E1 is dense and
A2: F is complete and
A3: dom f = E1 and
A4: f is_uniformly_continuous_on E1 ; :: thesis: ( ex g being Function of E,F st
( g | E1 = f & g is_uniformly_continuous_on the carrier of E & ( for x being Point of E ex seq being sequence of E st
( rng seq c= E1 & seq is convergent & lim seq = x & f /* seq is convergent & g . x = lim (f /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds
( f /* seq is convergent & g . x = lim (f /* seq) ) ) ) & ( for g1, g2 being Function of E,F st g1 | E1 = f & g1 is_continuous_on the carrier of E & g2 | E1 = f & g2 is_continuous_on the carrier of E holds
g1 = g2 ) )
A6: for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent holds
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* seq) . m) - ((f /* seq) . n)).|| < s
proof
let x be Point of E; :: thesis: for seq being sequence of E st rng seq c= E1 & seq is convergent holds
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* seq) . m) - ((f /* seq) . n)).|| < s
let seq be sequence of E; :: thesis: ( rng seq c= E1 & seq is convergent implies for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* seq) . m) - ((f /* seq) . n)).|| < s )
assume that
A7: rng seq c= E1 and
A8: seq is convergent ; :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* seq) . m) - ((f /* seq) . n)).|| < s
set fseq = f /* seq;
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* seq) . m) - ((f /* seq) . n)).|| < r )
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* seq) . m) - ((f /* seq) . n)).|| < r
then consider s being Real such that
A10: ( 0 < s & ( for x1, x2 being Point of E st x1 in E1 & x2 in E1 & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) by A4, NFCONT_2:def 1;
consider n being Nat such that
A11: for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s by A8, A10, LOPBAN_3:4;
take n ; :: thesis: for m being Nat st n <= m holds
||.(((f /* seq) . m) - ((f /* seq) . n)).|| < r
let m be Nat; :: thesis: ( n <= m implies ||.(((f /* seq) . m) - ((f /* seq) . n)).|| < r )
assume n <= m ; :: thesis: ||.(((f /* seq) . m) - ((f /* seq) . n)).|| < r
then A13: ||.((seq . m) - (seq . n)).|| < s by A11;
A14: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
B14: ( seq . m in rng seq & seq . n in rng seq ) by FUNCT_2:4, ORDINAL1:def 12;
( f /. (seq . m) = (f /* seq) . m & f /. (seq . n) = (f /* seq) . n ) by A3, A7, A14, FUNCT_2:109;
hence ||.(((f /* seq) . m) - ((f /* seq) . n)).|| < r by A7, A10, A13, B14; :: thesis: verum
end;
A16: for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent holds
f /* seq is convergent
proof
let x be Point of E; :: thesis: for seq being sequence of E st rng seq c= E1 & seq is convergent holds
f /* seq is convergent
let seq be sequence of E; :: thesis: ( rng seq c= E1 & seq is convergent implies f /* seq is convergent )
assume that
A17: rng seq c= E1 and
A18: seq is convergent ; :: thesis: f /* seq is convergent
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* seq) . m) - ((f /* seq) . n)).|| < s by A6, A17, A18;
hence f /* seq is convergent by A2, LOPBAN_1:def 15, LOPBAN_3:5; :: thesis: verum
end;
A19: for x being Point of E
for seq1, seq2 being sequence of E st rng seq1 c= E1 & seq1 is convergent & lim seq1 = x & rng seq2 c= E1 & seq2 is convergent & lim seq2 = x holds
lim (f /* seq1) = lim (f /* seq2)
proof
let x be Point of E; :: thesis: for seq1, seq2 being sequence of E st rng seq1 c= E1 & seq1 is convergent & lim seq1 = x & rng seq2 c= E1 & seq2 is convergent & lim seq2 = x holds
lim (f /* seq1) = lim (f /* seq2)
let seq1, seq2 be sequence of E; :: thesis: ( rng seq1 c= E1 & seq1 is convergent & lim seq1 = x & rng seq2 c= E1 & seq2 is convergent & lim seq2 = x implies lim (f /* seq1) = lim (f /* seq2) )
assume that
A20: ( rng seq1 c= E1 & seq1 is convergent & lim seq1 = x ) and
A21: ( rng seq2 c= E1 & seq2 is convergent & lim seq2 = x ) ; :: thesis: lim (f /* seq1) = lim (f /* seq2)
deffunc H1( Nat) -> Element of the carrier of E = seq1 . $1;
deffunc H2( Nat) -> Element of the carrier of E = seq2 . $1;
consider s being sequence of the carrier of E such that
A22: for n being Nat holds
( s . (2 * n) = H1(n) & s . ((2 * n) + 1) = H2(n) ) from INTEGR20:sch 1();
B23: now :: thesis: for y being object st y in rng s holds
y in E1
let y be object ; :: thesis: ( y in rng s implies b1 in E1 )
assume y in rng s ; :: thesis: b1 in E1
then consider i being object such that
A23: ( i in NAT & y = s . i ) by FUNCT_2:11;
reconsider i = i as Nat by A23;
consider k being Nat such that
A24: ( i = 2 * k or i = (2 * k) + 1 ) by INTEGR20:14;
reconsider k1 = k, i1 = i as Element of NAT by ORDINAL1:def 12;
per cases ( i = 2 * k1 or i = (2 * k1) + 1 ) by A24;
suppose i = 2 * k1 ; :: thesis: b1 in E1
then s . i = seq1 . k1 by A22;
then s . i in rng seq1 by FUNCT_2:4;
hence y in E1 by A20, A23; :: thesis: verum
end;
suppose i = (2 * k1) + 1 ; :: thesis: b1 in E1
then s . i = seq2 . k1 by A22;
then s . i in rng seq2 by FUNCT_2:4;
hence y in E1 by A21, A23; :: thesis: verum
end;
end;
end;
then A28: rng s c= E1 by TARSKI:def 3;
now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((s . m) - x).|| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.((s . b5) - x).|| < b3 )
assume A30: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((s . b5) - x).|| < b3
then consider n1 being Nat such that
A31: for m being Nat st n1 <= m holds
||.((seq1 . m) - x).|| < p by A20, NORMSP_1:def 7;
consider n2 being Nat such that
A32: for m being Nat st n2 <= m holds
||.((seq2 . m) - x).|| < p by A21, A30, NORMSP_1:def 7;
reconsider n3 = max (n1,n2) as Nat by TARSKI:1;
A33: ( n1 <= n3 & n2 <= n3 ) by XXREAL_0:25;
reconsider n = (2 * n3) + 1 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
||.((s . b4) - x).|| < b2
let m be Nat; :: thesis: ( n <= m implies ||.((s . b3) - x).|| < b1 )
assume A34: n <= m ; :: thesis: ||.((s . b3) - x).|| < b1
consider k being Nat such that
A35: ( m = 2 * k or m = (2 * k) + 1 ) by INTEGR20:14;
reconsider k1 = k, m1 = m as Element of NAT by ORDINAL1:def 12;
per cases ( m = 2 * k1 or m = (2 * k) + 1 ) by A35;
suppose A36: m = 2 * k1 ; :: thesis: ||.((s . b3) - x).|| < b1
then A37: s . m = seq1 . k1 by A22;
A38: 2 * n3 <= (2 * k) - 1 by A34, A36, XREAL_1:19;
(2 * k) - 1 < ((2 * k) - 1) + 1 by XREAL_1:145;
then 2 * n3 <= 2 * k by A38, XXREAL_0:2;
then (2 * n3) / 2 <= (2 * k) / 2 by XREAL_1:72;
then n1 <= k by A33, XXREAL_0:2;
hence ||.((s . m) - x).|| < p by A31, A37; :: thesis: verum
end;
suppose A39: m = (2 * k) + 1 ; :: thesis: ||.((s . b3) - x).|| < b1
then A40: s . m1 = seq2 . k1 by A22;
((2 * n3) + 1) - 1 <= ((2 * k) + 1) - 1 by A34, A39, XREAL_1:13;
then (2 * n3) / 2 <= (2 * k) / 2 by XREAL_1:72;
then n2 <= k by A33, XXREAL_0:2;
hence ||.((s . m) - x).|| < p by A32, A40; :: thesis: verum
end;
end;
end;
then A42: f /* s is convergent by A16, A28, NORMSP_1:def 6;
for i being Nat holds
( (f /* s) . (2 * i) = (f /* seq1) . i & (f /* s) . ((2 * i) + 1) = (f /* seq2) . i )
proof
let i be Nat; :: thesis: ( (f /* s) . (2 * i) = (f /* seq1) . i & (f /* s) . ((2 * i) + 1) = (f /* seq2) . i )
A43: i in NAT by ORDINAL1:def 12;
2 * i in NAT by ORDINAL1:def 12;
hence (f /* s) . (2 * i) = f /. (s . (2 * i)) by A3, B23, FUNCT_2:109, TARSKI:def 3
.= f /. (seq1 . i) by A22
.= (f /* seq1) . i by A3, A20, A43, FUNCT_2:109 ;
:: thesis: (f /* s) . ((2 * i) + 1) = (f /* seq2) . i
thus (f /* s) . ((2 * i) + 1) = f /. (s . ((2 * i) + 1)) by A3, B23, FUNCT_2:109, TARSKI:def 3
.= f /. (seq2 . i) by A22
.= (f /* seq2) . i by A3, A21, A43, FUNCT_2:109 ; :: thesis: verum
end;
then ( lim (f /* seq1) = lim (f /* s) & lim (f /* seq2) = lim (f /* s) ) by A42, INTEGR20:18;
hence lim (f /* seq1) = lim (f /* seq2) ; :: thesis: verum
end;
defpred S1[ object , object ] means ex seq being sequence of E st
( rng seq c= E1 & seq is convergent & lim seq = $1 & f /* seq is convergent & $2 = lim (f /* seq) );
A46: for x being Element of E ex y being Element of F st S1[x,y]
proof
let x be Element of E; :: thesis: ex y being Element of F st S1[x,y]
consider seq being sequence of E such that
A47: ( rng seq c= E1 & seq is convergent & lim seq = x ) by A1, NORMSP_3:14;
take y = lim (f /* seq); :: thesis: S1[x,y]
thus S1[x,y] by A16, A47; :: thesis: verum
end;
consider g being Function of E,F such that
A49: for x being Element of E holds S1[x,g . x] from FUNCT_2:sch 3(A46);
 A50: dom g = the carrier of E by FUNCT_2:def 1;
A51: dom f = the carrier of E /\ E1 by A3, XBOOLE_1:28
.= (dom g) /\ E1 by FUNCT_2:def 1 ;
A52: f is_continuous_on E1 by A4, NFCONT_2:7;
for x being object st x in dom f holds
f . x = g . x
proof
let x0 be object ; :: thesis: ( x0 in dom f implies f . x0 = g . x0 )
assume A53: x0 in dom f ; :: thesis: f . x0 = g . x0
then A54: ( x0 in dom g & x0 in E1 ) by A51, XBOOLE_0:def 4;
reconsider x = x0 as Point of E by A53;
reconsider seq1 = NAT --> x as sequence of E ;
for n being Nat holds seq1 . n = x by FUNCOP_1:7, ORDINAL1:def 12;
then A56: ( seq1 is convergent & lim seq1 = x ) by NORMSP_3:23;
A58: rng seq1 c= E1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng seq1 or y in E1 )
assume y in rng seq1 ; :: thesis: y in E1
then consider i being object such that
A57: ( i in NAT & y = seq1 . i ) by FUNCT_2:11;
reconsider i = i as Nat by A57;
thus y in E1 by A54, A57, FUNCOP_1:7; :: thesis: verum
end;
then ( f /* seq1 is convergent & lim (f /* seq1) = f /. (lim seq1) ) by A52, A54, A56, NFCONT_1:18;
then A59: lim (f /* seq1) = f . x by A53, A56, PARTFUN1:def 6;
consider seq2 being sequence of E such that
A60: ( rng seq2 c= E1 & seq2 is convergent & lim seq2 = x & f /* seq2 is convergent & g . x = lim (f /* seq2) ) by A49;
thus f . x0 = g . x0 by A19, A56, A58, A59, A60; :: thesis: verum
end;
then A61: g | E1 = f by A51, FUNCT_1:46;
A62: for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds
( f /* seq is convergent & g . x = lim (f /* seq) )
proof
let x be Point of E; :: thesis: for seq being sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds
( f /* seq is convergent & g . x = lim (f /* seq) )
let seq be sequence of E; :: thesis: ( rng seq c= E1 & seq is convergent & lim seq = x implies ( f /* seq is convergent & g . x = lim (f /* seq) ) )
assume A63: ( rng seq c= E1 & seq is convergent & lim seq = x ) ; :: thesis: ( f /* seq is convergent & g . x = lim (f /* seq) )
consider seq1 being sequence of E such that
A64: ( rng seq1 c= E1 & seq1 is convergent & lim seq1 = x & f /* seq1 is convergent & g . x = lim (f /* seq1) ) by A49;
thus f /* seq is convergent by A16, A63; :: thesis: g . x = lim (f /* seq)
thus g . x = lim (f /* seq) by A19, A63, A64; :: thesis: verum
end;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of E st x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s holds
||.((g /. x1) - (g /. x2)).|| < r ) )
proof
let r0 be Real; :: thesis: ( 0 < r0 implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of E st x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s holds
||.((g /. x1) - (g /. x2)).|| < r0 ) ) )
assume A65: 0 < r0 ; :: thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Point of E st x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s holds
||.((g /. x1) - (g /. x2)).|| < r0 ) )
set r1 = r0 / 2;
A66: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A65, XREAL_1:215, XREAL_1:216;
set r = (r0 / 2) / 3;
A67: ( 0 < (r0 / 2) / 3 & (r0 / 2) / 3 < r0 / 2 ) by A66, XREAL_1:221, XREAL_1:222;
consider s0 being Real such that
A68: ( 0 < s0 & ( for x1, x2 being Point of E st x1 in E1 & x2 in E1 & ||.(x1 - x2).|| < s0 holds
||.((f /. x1) - (f /. x2)).|| < (r0 / 2) / 3 ) ) by A4, A66, NFCONT_2:def 1, XREAL_1:222;
set s = s0 / 3;
A69: ( 0 < s0 / 3 & s0 / 3 < s0 ) by A68, XREAL_1:221, XREAL_1:222;
take s0 / 3 ; :: thesis: ( 0 < s0 / 3 & ( for x1, x2 being Point of E st x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s0 / 3 holds
||.((g /. x1) - (g /. x2)).|| < r0 ) )
thus 0 < s0 / 3 by A68, XREAL_1:222; :: thesis: for x1, x2 being Point of E st x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s0 / 3 holds
||.((g /. x1) - (g /. x2)).|| < r0
let x1, x2 be Point of E; :: thesis: ( x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s0 / 3 implies ||.((g /. x1) - (g /. x2)).|| < r0 )
assume A70: ( x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s0 / 3 ) ; :: thesis: ||.((g /. x1) - (g /. x2)).|| < r0
consider seq1 being sequence of E such that
A71: ( rng seq1 c= E1 & seq1 is convergent & lim seq1 = x1 & f /* seq1 is convergent & g . x1 = lim (f /* seq1) ) by A49;
consider M10 being Nat such that
A72: for n being Nat st M10 <= n holds
||.((seq1 . n) - x1).|| < s0 / 3 by A69, A71, NORMSP_1:def 7;
consider M11 being Nat such that
A73: for n being Nat st M11 <= n holds
||.(((f /* seq1) . n) - (g . x1)).|| < (r0 / 2) / 3 by A67, A71, NORMSP_1:def 7;
set M1 = M10 + M11;
A74: ( M10 + 0 <= M10 + M11 & M11 + 0 <= M10 + M11 ) by XREAL_1:7;
consider seq2 being sequence of E such that
A75: ( rng seq2 c= E1 & seq2 is convergent & lim seq2 = x2 & f /* seq2 is convergent & g . x2 = lim (f /* seq2) ) by A49;
consider M20 being Nat such that
A76: for n being Nat st M20 <= n holds
||.((seq2 . n) - x2).|| < s0 / 3 by A69, A75, NORMSP_1:def 7;
consider M21 being Nat such that
A77: for n being Nat st M21 <= n holds
||.(((f /* seq2) . n) - (g . x2)).|| < (r0 / 2) / 3 by A67, A75, NORMSP_1:def 7;
set M2 = M20 + M21;
A78: ( M20 + 0 <= M20 + M21 & M21 + 0 <= M20 + M21 ) by XREAL_1:7;
set n = (M10 + M11) + (M20 + M21);
A82: ( ||.((seq1 . ((M10 + M11) + (M20 + M21))) - x1).|| < s0 / 3 & ||.(((f /* seq1) . ((M10 + M11) + (M20 + M21))) - (g . x1)).|| < (r0 / 2) / 3 ) by A72, A73, A74, XREAL_1:7;
A83: ( ||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| < s0 / 3 & ||.(((f /* seq2) . ((M10 + M11) + (M20 + M21))) - (g . x2)).|| < (r0 / 2) / 3 ) by A76, A77, A78, XREAL_1:7;
(seq2 . ((M10 + M11) + (M20 + M21))) - (seq1 . ((M10 + M11) + (M20 + M21))) = (((seq2 . ((M10 + M11) + (M20 + M21))) - x2) + x2) - (seq1 . ((M10 + M11) + (M20 + M21))) by RLVECT_4:1
.= (((seq2 . ((M10 + M11) + (M20 + M21))) - x2) + ((x2 - x1) + x1)) - (seq1 . ((M10 + M11) + (M20 + M21))) by RLVECT_4:1
.= ((((seq2 . ((M10 + M11) + (M20 + M21))) - x2) + (x2 - x1)) + x1) - (seq1 . ((M10 + M11) + (M20 + M21))) by RLVECT_1:def 3
.= (((seq2 . ((M10 + M11) + (M20 + M21))) - x2) + (x2 - x1)) + (x1 - (seq1 . ((M10 + M11) + (M20 + M21)))) by RLVECT_1:28 ;
then A84: ||.((seq2 . ((M10 + M11) + (M20 + M21))) - (seq1 . ((M10 + M11) + (M20 + M21)))).|| <= ||.(((seq2 . ((M10 + M11) + (M20 + M21))) - x2) + (x2 - x1)).|| + ||.(x1 - (seq1 . ((M10 + M11) + (M20 + M21)))).|| by NORMSP_1:def 1;
||.(((seq2 . ((M10 + M11) + (M20 + M21))) - x2) + (x2 - x1)).|| <= ||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| + ||.(x2 - x1).|| by NORMSP_1:def 1;
then ||.(((seq2 . ((M10 + M11) + (M20 + M21))) - x2) + (x2 - x1)).|| + ||.(x1 - (seq1 . ((M10 + M11) + (M20 + M21)))).|| <= (||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| + ||.(x2 - x1).||) + ||.(x1 - (seq1 . ((M10 + M11) + (M20 + M21)))).|| by XREAL_1:7;
then A85: ||.((seq2 . ((M10 + M11) + (M20 + M21))) - (seq1 . ((M10 + M11) + (M20 + M21)))).|| <= (||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| + ||.(x2 - x1).||) + ||.(x1 - (seq1 . ((M10 + M11) + (M20 + M21)))).|| by A84, XXREAL_0:2;
||.(x2 - x1).|| < s0 / 3 by A70, NORMSP_1:7;
then A86: ||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| + ||.(x2 - x1).|| < (s0 / 3) + (s0 / 3) by A83, XREAL_1:8;
||.(x1 - (seq1 . ((M10 + M11) + (M20 + M21)))).|| < s0 / 3 by A82, NORMSP_1:7;
then (||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| + ||.(x2 - x1).||) + ||.(x1 - (seq1 . ((M10 + M11) + (M20 + M21)))).|| < ((s0 / 3) + (s0 / 3)) + (s0 / 3) by A86, XREAL_1:8;
then ||.((seq2 . ((M10 + M11) + (M20 + M21))) - (seq1 . ((M10 + M11) + (M20 + M21)))).|| < ((s0 / 3) + (s0 / 3)) + (s0 / 3) by A85, XXREAL_0:2;
then A87: ||.((seq1 . ((M10 + M11) + (M20 + M21))) - (seq2 . ((M10 + M11) + (M20 + M21)))).|| < ((s0 / 3) + (s0 / 3)) + (s0 / 3) by NORMSP_1:7;
A88: (M10 + M11) + (M20 + M21) in NAT by ORDINAL1:def 12;
( seq2 . ((M10 + M11) + (M20 + M21)) in rng seq2 & seq1 . ((M10 + M11) + (M20 + M21)) in rng seq1 ) by FUNCT_2:4, ORDINAL1:def 12;
then A89: ||.((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21))))).|| < (r0 / 2) / 3 by A68, A71, A75, A87;
(g /. x1) - (g /. x2) = (((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))) + (f /. (seq1 . ((M10 + M11) + (M20 + M21))))) - (g /. x2) by RLVECT_4:1
.= (((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))) + (((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21))))) + (f /. (seq2 . ((M10 + M11) + (M20 + M21)))))) - (g /. x2) by RLVECT_4:1
.= ((((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))) + ((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21)))))) + (f /. (seq2 . ((M10 + M11) + (M20 + M21))))) - (g /. x2) by RLVECT_1:def 3
.= (((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))) + ((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21)))))) + ((f /. (seq2 . ((M10 + M11) + (M20 + M21)))) - (g /. x2)) by RLVECT_1:28 ;
then A90: ||.((g /. x1) - (g /. x2)).|| <= ||.(((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))) + ((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21)))))).|| + ||.((f /. (seq2 . ((M10 + M11) + (M20 + M21)))) - (g /. x2)).|| by NORMSP_1:def 1;
||.(((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))) + ((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21)))))).|| <= ||.((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))).|| + ||.((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21))))).|| by NORMSP_1:def 1;
then ||.(((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))) + ((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21)))))).|| + ||.((f /. (seq2 . ((M10 + M11) + (M20 + M21)))) - (g /. x2)).|| <= (||.((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))).|| + ||.((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21))))).||) + ||.((f /. (seq2 . ((M10 + M11) + (M20 + M21)))) - (g /. x2)).|| by XREAL_1:7;
then A91: ||.((g /. x1) - (g /. x2)).|| <= (||.((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))).|| + ||.((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21))))).||) + ||.((f /. (seq2 . ((M10 + M11) + (M20 + M21)))) - (g /. x2)).|| by A90, XXREAL_0:2;
A92: ||.((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))).|| = ||.((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (g . x1)).|| by NORMSP_1:7
.= ||.(((f /* seq1) . ((M10 + M11) + (M20 + M21))) - (g . x1)).|| by A3, A71, A88, FUNCT_2:109 ;
A93: ||.((f /. (seq2 . ((M10 + M11) + (M20 + M21)))) - (g /. x2)).|| = ||.(((f /* seq2) . ((M10 + M11) + (M20 + M21))) - (g . x2)).|| by A3, A75, A88, FUNCT_2:109;
||.((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))).|| + ||.((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21))))).|| <= ((r0 / 2) / 3) + ((r0 / 2) / 3) by A82, A89, A92, XREAL_1:7;
then (||.((g /. x1) - (f /. (seq1 . ((M10 + M11) + (M20 + M21))))).|| + ||.((f /. (seq1 . ((M10 + M11) + (M20 + M21)))) - (f /. (seq2 . ((M10 + M11) + (M20 + M21))))).||) + ||.((f /. (seq2 . ((M10 + M11) + (M20 + M21)))) - (g /. x2)).|| < (((r0 / 2) / 3) + ((r0 / 2) / 3)) + ((r0 / 2) / 3) by A83, A93, XREAL_1:8;
then ||.((g /. x1) - (g /. x2)).|| < (((r0 / 2) / 3) + ((r0 / 2) / 3)) + ((r0 / 2) / 3) by A91, XXREAL_0:2;
hence ||.((g /. x1) - (g /. x2)).|| < r0 by A66, XXREAL_0:2; :: thesis: verum
end;
hence ex g being Function of E,F st
( g | E1 = f & g is_uniformly_continuous_on the carrier of E & ( for x being Point of E ex seq being sequence of E st
( rng seq c= E1 & seq is convergent & lim seq = x & f /* seq is convergent & g . x = lim (f /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds
( f /* seq is convergent & g . x = lim (f /* seq) ) ) ) by A49, A50, A61, A62, NFCONT_2:def 1; :: thesis: for g1, g2 being Function of E,F st g1 | E1 = f & g1 is_continuous_on the carrier of E & g2 | E1 = f & g2 is_continuous_on the carrier of E holds
g1 = g2
let g1, g2 be Function of E,F; :: thesis: ( g1 | E1 = f & g1 is_continuous_on the carrier of E & g2 | E1 = f & g2 is_continuous_on the carrier of E implies g1 = g2 )
assume that
A95: ( g1 | E1 = f & g1 is_continuous_on the carrier of E ) and
A96: ( g2 | E1 = f & g2 is_continuous_on the carrier of E ) ; :: thesis: g1 = g2
for x being Element of E holds g1 . x = g2 . x
proof
let x be Element of E; :: thesis: g1 . x = g2 . x
consider seq being sequence of E such that
A97: ( rng seq c= E1 & seq is convergent & lim seq = x ) by A1, NORMSP_3:14;
A106: g1 /* seq = f /* seq by A3, A95, A97, FUNCT_2:117
.= g2 /* seq by A3, A96, A97, FUNCT_2:117 ;
thus g1 . x = g1 /. (lim seq) by A97
.= lim (g2 /* seq) by A95, A97, A106, NFCONT_1:18
.= g2 /. x by A96, A97, NFCONT_1:18
.= g2 . x ; :: thesis: verum
end;
hence g1 = g2 by FUNCT_2:def 8; :: thesis: verum