theorem :: RFINSEQ2:5

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