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 ;
consider n being Nat such that
A11: for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s by ;
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 ;
( f /. (seq . m) = (f /* seq) . m & f /. (seq . n) = (f /* seq) . n ) by ;
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 ; :: 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
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 ; :: 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 ; :: 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 ;
consider n2 being Nat such that
A32: for m being Nat st n2 <= m holds
||.((seq2 . m) - x).|| < p by ;
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 ;
(2 * k) - 1 < ((2 * k) - 1) + 1 by XREAL_1:145;
then 2 * n3 <= 2 * k by ;
then (2 * n3) / 2 <= (2 * k) / 2 by XREAL_1:72;
then n1 <= k by ;
hence ||.((s . m) - x).|| < p by ; :: 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 ;
then (2 * n3) / 2 <= (2 * k) / 2 by XREAL_1:72;
then n2 <= k by ;
hence ||.((s . m) - x).|| < p by ; :: thesis: verum
end;
end;
end;
then A42: f /* s is convergent by ;
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
.= f /. (seq1 . i) by A22
.= (f /* seq1) . i by ;
:: thesis: (f /* s) . ((2 * i) + 1) = (f /* seq2) . i
thus (f /* s) . ((2 * i) + 1) = f /. (s . ((2 * i) + 1)) by
.= f /. (seq2 . i) by A22
.= (f /* seq2) . i by ; :: thesis: verum
end;
then ( lim (f /* seq1) = lim (f /* s) & lim (f /* seq2) = lim (f /* s) ) by ;
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 ;
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 A50: dom g = the carrier of E by FUNCT_2:def 1;
A51: dom f = the carrier of E /\ E1 by
.= (dom g) /\ E1 by FUNCT_2:def 1 ;
A52: f is_continuous_on E1 by ;
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 ;
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 ;
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 ; :: thesis: verum
end;
then ( f /* seq1 is convergent & lim (f /* seq1) = f /. (lim seq1) ) by ;
then A59: lim (f /* seq1) = f . x by ;
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 ;
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 ; :: thesis: g . x = lim (f /* seq)
thus g . x = lim (f /* seq) by ; :: 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 ;
set r = (r0 / 2) / 3;
A67: ( 0 < (r0 / 2) / 3 & (r0 / 2) / 3 < r0 / 2 ) by ;
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 ;
set s = s0 / 3;
A69: ( 0 < s0 / 3 & s0 / 3 < s0 ) by ;
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 ; :: 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 ;
consider M11 being Nat such that
A73: for n being Nat st M11 <= n holds
||.(((f /* seq1) . n) - (g . x1)).|| < (r0 / 2) / 3 by ;
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 ;
consider M21 being Nat such that
A77: for n being Nat st M21 <= n holds
||.(((f /* seq2) . n) - (g . x2)).|| < (r0 / 2) / 3 by ;
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 ;
A83: ( ||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| < s0 / 3 & ||.(((f /* seq2) . ((M10 + M11) + (M20 + M21))) - (g . x2)).|| < (r0 / 2) / 3 ) by ;
(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 ;
||.(x2 - x1).|| < s0 / 3 by ;
then A86: ||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| + ||.(x2 - x1).|| < (s0 / 3) + (s0 / 3) by ;
||.(x1 - (seq1 . ((M10 + M11) + (M20 + M21)))).|| < s0 / 3 by ;
then (||.((seq2 . ((M10 + M11) + (M20 + M21))) - x2).|| + ||.(x2 - x1).||) + ||.(x1 - (seq1 . ((M10 + M11) + (M20 + M21)))).|| < ((s0 / 3) + (s0 / 3)) + (s0 / 3) by ;
then ||.((seq2 . ((M10 + M11) + (M20 + M21))) - (seq1 . ((M10 + M11) + (M20 + M21)))).|| < ((s0 / 3) + (s0 / 3)) + (s0 / 3) by ;
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 ;
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 ;
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 ;
A93: ||.((f /. (seq2 . ((M10 + M11) + (M20 + M21)))) - (g /. x2)).|| = ||.(((f /* seq2) . ((M10 + M11) + (M20 + M21))) - (g . x2)).|| by ;
||.((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 ;
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 ;
then ||.((g /. x1) - (g /. x2)).|| < (((r0 / 2) / 3) + ((r0 / 2) / 3)) + ((r0 / 2) / 3) by ;
hence ||.((g /. x1) - (g /. x2)).|| < r0 by ; :: 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 ; :: 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 ;
A106: g1 /* seq = f /* seq by
.= g2 /* seq by ;
thus g1 . x = g1 /. (lim seq) by A97
.= lim (g2 /* seq) by
.= g2 /. x by
.= g2 . x ; :: thesis: verum
end;
hence g1 = g2 by FUNCT_2:def 8; :: thesis: verum