let X, Y be RealNormSpace; :: thesis: for T being non empty PartFunc of X,Y

for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds

T is closed

let T be non empty PartFunc of X,Y; :: thesis: for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds

T is closed

let T0 be LinearOperator of X,Y; :: thesis: ( T0 is Lipschitzian & dom T is closed & T = T0 implies T is closed )

assume A1: ( T0 is Lipschitzian & dom T is closed & T = T0 ) ; :: thesis: T is closed

then A2: T is_continuous_in 0. X by Th5, Th6;

for seq being sequence of X st rng seq c= dom T & seq is convergent & T /* seq is convergent holds

( lim seq in dom T & lim (T /* seq) = T . (lim seq) )

for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds

T is closed

let T be non empty PartFunc of X,Y; :: thesis: for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds

T is closed

let T0 be LinearOperator of X,Y; :: thesis: ( T0 is Lipschitzian & dom T is closed & T = T0 implies T is closed )

assume A1: ( T0 is Lipschitzian & dom T is closed & T = T0 ) ; :: thesis: T is closed

then A2: T is_continuous_in 0. X by Th5, Th6;

for seq being sequence of X st rng seq c= dom T & seq is convergent & T /* seq is convergent holds

( lim seq in dom T & lim (T /* seq) = T . (lim seq) )

proof

hence
T is closed
by Th12; :: thesis: verum
let seq be sequence of X; :: thesis: ( rng seq c= dom T & seq is convergent & T /* seq is convergent implies ( lim seq in dom T & lim (T /* seq) = T . (lim seq) ) )

assume A3: ( rng seq c= dom T & seq is convergent & T /* seq is convergent ) ; :: thesis: ( lim seq in dom T & lim (T /* seq) = T . (lim seq) )

A4: T is_continuous_in lim seq by A1, A2, Th4;

T /. (lim seq) = T . (lim seq) by A1, A3, NFCONT_1:def 3, PARTFUN1:def 6;

hence ( lim seq in dom T & lim (T /* seq) = T . (lim seq) ) by A3, A4, NFCONT_1:def 5; :: thesis: verum

end;assume A3: ( rng seq c= dom T & seq is convergent & T /* seq is convergent ) ; :: thesis: ( lim seq in dom T & lim (T /* seq) = T . (lim seq) )

A4: T is_continuous_in lim seq by A1, A2, Th4;

T /. (lim seq) = T . (lim seq) by A1, A3, NFCONT_1:def 3, PARTFUN1:def 6;

hence ( lim seq in dom T & lim (T /* seq) = T . (lim seq) ) by A3, A4, NFCONT_1:def 5; :: thesis: verum