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

for seq being sequence of E st rng seq c= E1 & seq is convergent holds

f /* seq is convergent

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)_{1}[ 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 S_{1}[x,y]

A49: for x being Element of E holds S_{1}[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

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

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

( 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

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

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

for seq being sequence of E st rng seq c= E1 & seq is convergent holds

f /* seq is convergent

proof

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

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

defpred S
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 H_{1}( Nat) -> Element of the carrier of E = seq1 . $1;

deffunc H_{2}( 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) = H_{1}(n) & s . ((2 * n) + 1) = H_{2}(n) )
from INTEGR20:sch 1();

for i being Nat holds

( (f /* s) . (2 * i) = (f /* seq1) . i & (f /* s) . ((2 * i) + 1) = (f /* seq2) . i )

hence lim (f /* seq1) = lim (f /* seq2) ; :: thesis: verum

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

deffunc H

consider s being sequence of the carrier of E such that

A22: for n being Nat holds

( s . (2 * n) = H

B23: now :: thesis: for y being object st y in rng s holds

y in E1

then A28:
rng s c= E1
by TARSKI:def 3;y in E1

let y be object ; :: thesis: ( y in rng s implies b_{1} in E1 )

assume y in rng s ; :: thesis: b_{1} 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;

end;assume y in rng s ; :: thesis: b

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;

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

then A42:
f /* s is convergent
by A16, A28, NORMSP_1:def 6;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 . b_{5}) - x).|| < b_{3} )

assume A30: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((s . b_{5}) - x).|| < b_{3}

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 . b_{4}) - x).|| < b_{2}

let m be Nat; :: thesis: ( n <= m implies ||.((s . b_{3}) - x).|| < b_{1} )

assume A34: n <= m ; :: thesis: ||.((s . b_{3}) - x).|| < b_{1}

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;

end;for m being Nat st n <= m holds

||.((s . b

assume A30: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((s . b

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

let m be Nat; :: thesis: ( n <= m implies ||.((s . b

assume A34: n <= m ; :: thesis: ||.((s . b

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;

end;

suppose A36:
m = 2 * k1
; :: thesis: ||.((s . b_{3}) - x).|| < b_{1}

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

suppose A39:
m = (2 * k) + 1
; :: thesis: ||.((s . b_{3}) - x).|| < b_{1}

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

for i being Nat holds

( (f /* s) . (2 * i) = (f /* seq1) . i & (f /* s) . ((2 * i) + 1) = (f /* seq2) . i )

proof

then
( lim (f /* seq1) = lim (f /* s) & lim (f /* seq2) = lim (f /* s) )
by A42, INTEGR20:18;
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;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

hence lim (f /* seq1) = lim (f /* seq2) ; :: thesis: verum

( 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 S

proof

consider g being Function of E,F such that
let x be Element of E; :: thesis: ex y being Element of F st S_{1}[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: S_{1}[x,y]

thus S_{1}[x,y]
by A16, A47; :: thesis: verum

end;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: S

thus S

A49: for x being Element of E holds S

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

then A61:
g | E1 = f
by A51, FUNCT_1:46;
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

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

then
( f /* seq1 is convergent & lim (f /* seq1) = f /. (lim seq1) )
by A52, A54, A56, NFCONT_1:18;
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;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

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

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

for r being Real st 0 < r holds
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;( 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

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

hence
ex g being Function of E,F st
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;( 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

( 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

hence
g1 = g2
by FUNCT_2:def 8; :: thesis: verum
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;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