let E, F be RealNormSpace; :: thesis:
let f be Function of E,F; :: thesis:
assume A1: f is isometric ; :: thesis:
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) )

let s1 be sequence of E; :: thesis:
assume that
A2: rng s1 c= dom f and
A3: s1 is convergent and
lim s1 in dom f ; :: thesis:
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

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
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:
let n be Nat; :: thesis:
A8: n in NAT by ORDINAL1:def 12;
assume m <= n ; :: thesis:
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:

end;

end;