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