theorem :: RFINSEQ2:8

for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds
min (f1 + f2) >= (min f1) + (min f2)