:: deftheorem defines complete CLVECT_2:def 11 :
for X being ComplexUnitarySpace holds
( X is complete iff for seq being sequence of X st seq is Cauchy holds
seq is convergent );