:: deftheorem Def13 defines complete CLOPBAN1:def 13 :
for X being ComplexNormSpace holds
( X is complete iff for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds
seq is convergent );