:: deftheorem defines min MEASUR12:def 4 :
for f being FinSequence of ExtREAL holds min f = f . (min_p f);