let X, Y be RealNormSpace; :: thesis:
let T be non empty PartFunc of X,Y; :: thesis:
let S be non empty PartFunc of Y,X; :: thesis:
assume A1: ( T is closed & T is one-to-one & S = T " ) ; :: thesis:
A2: ( rng T = dom S & dom T = rng S ) by A1, FUNCT_1:33;
for seq being sequence of Y st rng seq c= dom S & seq is convergent & S /* seq is convergent holds
( lim seq in dom S & lim (S /* seq) = S . (lim seq) )

let seq be sequence of Y; :: thesis:
assume A3: ( rng seq c= dom S & seq is convergent & S /* seq is convergent ) ; :: thesis:
set seq1 = S /* seq;
A4: rng (S /* seq) c= dom T

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (S /* seq) ; :: thesis:
then consider i being object such that
A5: ( i in dom (S /* seq) & x = (S /* seq) . i ) by FUNCT_1:def 3;
reconsider i = i as Nat by A5;
S . (seq . i) in rng S by FUNCT_1:3, A3, NFCONT_1:5;
hence x in dom T by A5, A2, A3, FUNCT_2:108; :: thesis:

end;

A6: T /* (S /* seq) = seq

let n be Element of NAT ; :: thesis:
thus (T /* (S /* seq)) . n = seq . n :: thesis:

A7: seq . n in rng T by A3, NFCONT_1:5, A2;
(T /* (S /* seq)) . n = T . ((S /* seq) . n) by A4, FUNCT_2:108
.= T . (S . (seq . n)) by A3, FUNCT_2:108
.= seq . n by A1, A7, FUNCT_1:35 ;
hence (T /* (S /* seq)) . n = seq . n ; :: thesis:

end;

hence T /* (S /* seq) = seq ; :: thesis:

end;

( lim (S /* seq) in dom T & lim (T /* (S /* seq)) = T . (lim (S /* seq)) ) by A1, A3, A4, A6, Th12;
hence ( lim seq in dom S & lim (S /* seq) = S . (lim seq) ) by A2, A6, FUNCT_1:3, A1, FUNCT_1:34; :: thesis:

end;