let f1, f2 be real-valued FinSequence; ( len f1 = len f2 & len f1 > 0 implies max (f1 + f2) <= (max f1) + (max f2) )
assume that
A1:
len f1 = len f2
and
A2:
len f1 > 0
; max (f1 + f2) <= (max f1) + (max f2)
A3:
len (f1 + f2) = len f1
by A1, RVSUM_1:115;
then A4:
max_p (f1 + f2) in dom (f1 + f2)
by A2, Def1;
then
( 1 <= max_p (f1 + f2) & max_p (f1 + f2) <= len (f1 + f2) )
by FINSEQ_3:25;
then A5:
max_p (f1 + f2) in Seg (len f1)
by A3, FINSEQ_1:1;
then
max_p (f1 + f2) in dom f2
by A1, FINSEQ_1:def 3;
then A6:
f2 . (max_p (f1 + f2)) <= f2 . (max_p f2)
by A1, A2, Def1;
max_p (f1 + f2) in dom f1
by A5, FINSEQ_1:def 3;
then A7:
f1 . (max_p (f1 + f2)) <= f1 . (max_p f1)
by A2, Def1;
max (f1 + f2) = (f1 . (max_p (f1 + f2))) + (f2 . (max_p (f1 + f2)))
by A4, VALUED_1:def 1;
hence
max (f1 + f2) <= (max f1) + (max f2)
by A7, A6, XREAL_1:7; verum