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 ;
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 ;
hence x in dom T by ; :: 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 ;
(T /* (S /* seq)) . n = T . ((S /* seq) . n) by
.= T . (S . (seq . n)) by
.= seq . n by ;
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 ; :: thesis: verum
end;
hence S is closed by Th12; :: thesis: verum