let X, Y be RealNormSpace; :: thesis: for T being non empty PartFunc of X,Y
for S being non empty PartFunc of Y,X st T is closed & T is one-to-one & S = T " holds
S is closed
let T be non empty PartFunc of X,Y; :: thesis: for S being non empty PartFunc of Y,X st T is closed & T is one-to-one & S = T " holds
S is closed
let S be non empty PartFunc of Y,X; :: thesis: ( T is closed & T is one-to-one & S = T " implies S is closed )
assume A1: ( T is closed & T is one-to-one & S = T " ) ; :: thesis: S is closed
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) )

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (S /* seq) or x in dom T )
assume x in rng (S /* seq) ; :: thesis: x in dom T
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: verum

end;

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

proof

now :: thesis: for n being Element of NAT holds (T /* (S /* seq)) . n = seq . n

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

proof

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: verum

end;

end;

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

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: verum

end;

hence S is closed by Th12; :: thesis: verum