:: deftheorem defines |. SEQ_4:def 13 :
for z being FinSequence of COMPLEX holds |.z.| = sqrt (Sum (sqr (abs z)));