theorem :: RFINSEQ2:6

for f being real-valued FinSequence
for r1, r2 being Real st f = <*r1,r2*> holds
( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )