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