for X, Y being RealNormSpace
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) ) )