:: deftheorem Def4 defines dist CLVECT_2:def 4 :
for X being ComplexUnitarySpace
for seq being sequence of X
for x being Point of X
for b₄ being Real_Sequence holds
( b₄ = dist (seq,x) iff for n being Nat holds b₄ . n = dist ((seq . n),x) );