let E, F be RealNormSpace; :: thesis: for f being Function of E,F st f is isometric holds

f is_continuous_on dom f

let f be Function of E,F; :: thesis: ( f is isometric implies f is_continuous_on dom f )

assume A1: f is isometric ; :: thesis: f is_continuous_on dom f

set X = dom f;

for s1 being sequence of E st rng s1 c= dom f & s1 is convergent & lim s1 in dom f holds

( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )

f is_continuous_on dom f

let f be Function of E,F; :: thesis: ( f is isometric implies f is_continuous_on dom f )

assume A1: f is isometric ; :: thesis: f is_continuous_on dom f

set X = dom f;

for s1 being sequence of E st rng s1 c= dom f & s1 is convergent & lim s1 in dom f holds

( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )

proof

hence
f is_continuous_on dom f
by NFCONT_1:18; :: thesis: verum
let s1 be sequence of E; :: thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 in dom f implies ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) )

assume that

A2: rng s1 c= dom f and

A3: s1 is convergent and

lim s1 in dom f ; :: thesis: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )

consider a being Point of E such that

A4: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((s1 . n) - a).|| < r by A3;

A5: a = lim s1 by A3, A4, NORMSP_1:def 7;

A6: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.(((f /* s1) . n) - (f . a)).|| < r

hence f /. (lim s1) = lim (f /* s1) by A5, A6, NORMSP_1:def 7; :: thesis: verum

end;assume that

A2: rng s1 c= dom f and

A3: s1 is convergent and

lim s1 in dom f ; :: thesis: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )

consider a being Point of E such that

A4: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((s1 . n) - a).|| < r by A3;

A5: a = lim s1 by A3, A4, NORMSP_1:def 7;

A6: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.(((f /* s1) . n) - (f . a)).|| < r

proof

thus
f /* s1 is convergent
by A6; :: thesis: f /. (lim s1) = lim (f /* s1)
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for n being Nat st m <= n holds

||.(((f /* s1) . n) - (f . a)).|| < r )

assume 0 < r ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.(((f /* s1) . n) - (f . a)).|| < r

then consider m being Nat such that

A7: for n being Nat st m <= n holds

||.((s1 . n) - a).|| < r by A4;

take m ; :: thesis: for n being Nat st m <= n holds

||.(((f /* s1) . n) - (f . a)).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.(((f /* s1) . n) - (f . a)).|| < r )

A8: n in NAT by ORDINAL1:def 12;

assume m <= n ; :: thesis: ||.(((f /* s1) . n) - (f . a)).|| < r

then A9: ||.((s1 . n) - a).|| < r by A7;

A10: ||.((f . (s1 . n)) - (f . a)).|| = ||.((s1 . n) - a).|| by A1;

f /* s1 = f * s1 by A2, FUNCT_2:def 11;

hence ||.(((f /* s1) . n) - (f . a)).|| < r by A9, A10, FUNCT_2:15, A8; :: thesis: verum

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

||.(((f /* s1) . n) - (f . a)).|| < r )

assume 0 < r ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.(((f /* s1) . n) - (f . a)).|| < r

then consider m being Nat such that

A7: for n being Nat st m <= n holds

||.((s1 . n) - a).|| < r by A4;

take m ; :: thesis: for n being Nat st m <= n holds

||.(((f /* s1) . n) - (f . a)).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.(((f /* s1) . n) - (f . a)).|| < r )

A8: n in NAT by ORDINAL1:def 12;

assume m <= n ; :: thesis: ||.(((f /* s1) . n) - (f . a)).|| < r

then A9: ||.((s1 . n) - a).|| < r by A7;

A10: ||.((f . (s1 . n)) - (f . a)).|| = ||.((s1 . n) - a).|| by A1;

f /* s1 = f * s1 by A2, FUNCT_2:def 11;

hence ||.(((f /* s1) . n) - (f . a)).|| < r by A9, A10, FUNCT_2:15, A8; :: thesis: verum

hence f /. (lim s1) = lim (f /* s1) by A5, A6, NORMSP_1:def 7; :: thesis: verum