:: deftheorem defines abs EUCLID:def 3 :
for x being real-valued FinSequence holds abs x = absreal * x;