:: deftheorem defines max MEASUR12:def 3 :
for f being FinSequence of ExtREAL holds max f = f . (max_p f);