:: deftheorem defines compact NCFCONT1:def 2 :
for CNS being ComplexNormSpace
for X being Subset of CNS holds
( X is compact iff for s1 being sequence of CNS st rng s1 c= X holds
ex s2 being sequence of CNS st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) );