theorem :: RFINSEQ2:7

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