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