theorem Th020: :: LOPBAN_8:1

for E, F being RealNormSpace
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 ) )