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

( 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

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

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

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

( lim seq = lim seq & lim (T /* seq) = lim (T /* seq) )
;
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;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

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

( 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

hence
T is closed
by NFCONT_1:def 3; :: thesis: verum
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_{1}[ 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_{1}[i,x]

A11: for x being Element of NAT holds S_{1}[x,seq . x]
from FUNCT_2:sch 3(A8);

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

( 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;assume A7: ( rng s1 c= graph T & s1 is convergent ) ; :: thesis: lim s1 in graph T

defpred S

A8: for i being Element of NAT ex x being Element of the carrier of X st S

proof

consider seq being sequence of X such that
let i be Element of NAT ; :: thesis: ex x being Element of the carrier of X st S_{1}[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_{1}[i,x]

thus S_{1}[i,x]
by A10, FUNCT_1:1, A9, A7; :: thesis: verum

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

thus S

A11: for x being Element of NAT holds S

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

y in dom T

then A15:
rng seq c= dom T
;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;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

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

then A17:
( seq is convergent & lim seq = x & T /* seq is convergent & lim (T /* seq) = y )
by A16, Th8, A7;
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;(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

( 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