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 ;
seq . i in rng seq by ;
then [(seq . i),((T /* seq) . i)] in T by ;
hence y in graph T by ; :: 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 ;
then [(lim seq),(lim (T /* seq))] in graph T by ;
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 S1[ 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 S1[i,x]
proof
let i be Element of NAT ; :: thesis: ex x being Element of the carrier of X st S1[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: S1[i,x]
thus S1[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 S1[x,seq . x] from
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 ;
s1 . i in rng s1 by ;
hence y in dom T by ; :: 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 ;
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 ; :: thesis: verum
end;
hence T is closed by NFCONT_1:def 3; :: thesis: verum