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) )

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

hence
S is closed
by Th12; :: thesis: verum
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

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;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

A6:
T /* (S /* seq) = seq
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;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

proof

end;

( lim (S /* seq) in dom T & lim (T /* (S /* seq)) = T . (lim (S /* seq)) )
by A1, A3, A4, A6, Th12;now :: thesis: for n being Element of NAT holds (T /* (S /* seq)) . n = seq . n

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

thus (T /* (S /* seq)) . n = seq . n :: thesis: verum

end;thus (T /* (S /* seq)) . n = seq . n :: thesis: verum

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