theorem :: GRAPH_2:61

for F, F1 being FinSequence of INT
for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds
F1 is_non_decreasing_on 1,k + 1