:: deftheorem defines abs SEQ_4:def 10 :
for z being FinSequence of COMPLEX holds abs z = abscomplex * z;