let f1, f2 be FinSequence of REAL ; :: thesis: ( len f1 = len f2 & len f1 > 0 implies max (f1 + f2) <= (max f1) + (max f2) )
assume A1: ( len f1 = len f2 & len f1 > 0 ) ; :: thesis: max (f1 + f2) <= (max f1) + (max f2)
then A2: len (f1 + f2) = len f1 by EUCLID_2:6;
then A3: max_p (f1 + f2) in dom (f1 + f2) by A1, Def1;
then A4: ( 1 <= max_p (f1 + f2) & max_p (f1 + f2) <= len (f1 + f2) ) by FINSEQ_3:27;
A5: max (f1 + f2) = (f1 . (max_p (f1 + f2))) + (f2 . (max_p (f1 + f2))) by A3, VALUED_1:def 1;
A6: max_p (f1 + f2) in Seg (len f1) by A2, A4, FINSEQ_1:3;
then max_p (f1 + f2) in dom f1 by FINSEQ_1:def 3;
then A7: f1 . (max_p (f1 + f2)) <= f1 . (max_p f1) by A1, Def1;
max_p (f1 + f2) in dom f2 by A1, A6, FINSEQ_1:def 3;
then f2 . (max_p (f1 + f2)) <= f2 . (max_p f2) by A1, Def1;
hence max (f1 + f2) <= (max f1) + (max f2) by A5, A7, XREAL_1:9; :: thesis: verum