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