let X, Y be RealNormSpace; :: thesis: for T being non empty PartFunc of X,Y holds
( T is closed iff 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) ) )
let T be non empty PartFunc of X,Y; :: thesis: ( T is closed iff 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) ) )

hereby :: thesis: ( ( 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) ) ) implies T is closed )

assume A1: T is closed ; :: thesis: 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) )
thus 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) ) :: thesis: verum

proof

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 A2: ( rng seq c= dom T & seq is convergent & T /* seq is convergent ) ; :: thesis: ( lim seq in dom T & lim (T /* seq) = T . (lim seq) )
set s1 = <:seq,(T /* seq):>;
A3: rng <:seq,(T /* seq):> c= graph T

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng <:seq,(T /* seq):> or y in graph T )
assume y in rng <:seq,(T /* seq):> ; :: thesis: y in graph T
then consider i being object such that
A4: ( i in NAT & <:seq,(T /* seq):> . i = y ) by FUNCT_2:11;
A5: (T /* seq) . i = T . (seq . i) by A4, A2, FUNCT_2:108;
seq . i in rng seq by A4, FUNCT_2:4;
then [(seq . i),((T /* seq) . i)] in T by A5, FUNCT_1:def 2, A2;
hence y in graph T by A4, FUNCT_3:59; :: thesis: verum

end;

( lim seq = lim seq & lim (T /* seq) = lim (T /* seq) ) ;
then ( <:seq,(T /* seq):> is convergent & lim <:seq,(T /* seq):> = [(lim seq),(lim (T /* seq))] ) by Th8, A2;
then [(lim seq),(lim (T /* seq))] in graph T by A1, NFCONT_1:def 3, A3;
hence ( lim seq in dom T & lim (T /* seq) = T . (lim seq) ) by FUNCT_1:1; :: thesis: verum

end;

end;

assume A6: 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) ) ; :: thesis: T is closed
for s1 being sequence of [:X,Y:] st rng s1 c= graph T & s1 is convergent holds
lim s1 in graph T

proof

let s1 be sequence of [:X,Y:]; :: thesis: ( rng s1 c= graph T & s1 is convergent implies lim s1 in graph T )
assume A7: ( rng s1 c= graph T & s1 is convergent ) ; :: thesis: lim s1 in graph T
defpred S₁[ set , set ] means [$2,(T . $2)] = s1 . $1;
A8: for i being Element of NAT ex x being Element of the carrier of X st S₁[i,x]

proof

let i be Element of NAT ; :: thesis: ex x being Element of the carrier of X st S₁[i,x]
A9: s1 . i in rng s1 by FUNCT_2:4;
consider x being Point of X, y being Point of Y such that
A10: s1 . i = [x,y] by PRVECT_3:18;
take x ; :: thesis: S₁[i,x]
thus S₁[i,x] by A10, FUNCT_1:1, A9, A7; :: thesis: verum

end;

consider seq being sequence of X such that
A11: for x being Element of NAT holds S₁[x,seq . x] from FUNCT_2:sch 3(A8);

A12: now :: thesis: for y being object st y in rng seq holds
y in dom T

let y be object ; :: thesis: ( y in rng seq implies y in dom T )
assume y in rng seq ; :: thesis: y in dom T
then consider i being object such that
A13: ( i in dom seq & y = seq . i ) by FUNCT_1:def 3;
A14: [(seq . i),(T . (seq . i))] = s1 . i by A13, A11;
s1 . i in rng s1 by A13, FUNCT_2:4;
hence y in dom T by A13, FUNCT_1:1, A14, A7; :: thesis: verum

end;

then A15: rng seq c= dom T ;
consider x being Point of X, y being Point of Y such that
A16: lim s1 = [x,y] by PRVECT_3:18;
s1 = <:seq,(T /* seq):>

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: s1 . n = <:seq,(T /* seq):> . n
(T /* seq) . n = T . (seq . n) by A12, TARSKI:def 3, FUNCT_2:108;
hence s1 . n = [(seq . n),((T /* seq) . n)] by A11
.= <:seq,(T /* seq):> . n by FUNCT_3:59 ;
:: thesis: verum

end;

then A17: ( seq is convergent & lim seq = x & T /* seq is convergent & lim (T /* seq) = y ) by A16, Th8, A7;
( lim seq in dom T & lim (T /* seq) = T . (lim seq) ) by A15, A6, A17;
hence lim s1 in graph T by A16, A17, FUNCT_1:1; :: thesis: verum

end;

hence T is closed by NFCONT_1:def 3; :: thesis: verum