:: deftheorem defines |. EUCLID:def 5 :
for f being real-valued FinSequence holds |.f.| = sqrt (Sum (sqr f));