let F, F1 be FinSequence of INT ; :: thesis: 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

let k, ma be Nat; :: thesis: ( 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))) implies F1 is_non_decreasing_on 1,k + 1 )
assume that
A1: k + 1 <= len F and
A2: ma = min_at (F,(k + 1),(len F)) and
A3: F is_split_at k and
A4: F is_non_decreasing_on 1,k and
A5: F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) ; :: thesis: F1 is_non_decreasing_on 1,k + 1
A6: 1 <= k + 1 by NAT_1:12;
set Fk = F +* ((k + 1),(F . ma));
A7: dom F1 = dom (F +* ((k + 1),(F . ma))) by ;
A8: dom (F +* ((k + 1),(F . ma))) = dom F by FUNCT_7:30;
then A9: k + 1 in dom F1 by ;
let i, j be Nat; :: according to FINSEQ_6:def 9 :: thesis: ( 1 <= i & i <= j & j <= k + 1 implies F1 . i <= F1 . j )
assume that
A10: 1 <= i and
A11: i <= j and
A12: j <= k + 1 ; :: thesis: F1 . i <= F1 . j
A13: j <= len F by ;
1 <= j by ;
then A14: j in dom F1 by ;
per cases ( j < k + 1 or j = k + 1 ) by ;
suppose A15: j < k + 1 ; :: thesis: F1 . i <= F1 . j
then i < k + 1 by ;
then i <> ma by A1, A2, A6, Th59;
then A16: F1 . i = (F +* ((k + 1),(F . ma))) . i by
.= F . i by ;
j <> ma by A1, A2, A6, A15, Th59;
then A17: F1 . j = (F +* ((k + 1),(F . ma))) . j by
.= F . j by ;
j <= k by ;
hence F1 . i <= F1 . j by A4, A10, A11, A16, A17; :: thesis: verum
end;
suppose A18: j = k + 1 ; :: thesis: F1 . i <= F1 . j
thus F1 . i <= F1 . j :: thesis: verum
proof
per cases ( i < j or i = j ) by ;
suppose A19: i < j ; :: thesis: F1 . i <= F1 . j
then i <> ma by A1, A2, A6, A18, Th59;
then A20: F1 . i = (F +* ((k + 1),(F . ma))) . i by
.= F . i by ;
A21: i <= k by ;
A22: k < j by ;
thus F1 . i <= F1 . j :: thesis: verum
proof
per cases ( k + 1 = ma or k + 1 <> ma ) ;
suppose k + 1 = ma ; :: thesis: F1 . i <= F1 . j
then F1 . j = F . (k + 1) by ;
hence F1 . i <= F1 . j by A1, A3, A10, A18, A20, A21, A22; :: thesis: verum
end;
suppose A23: k + 1 <> ma ; :: thesis: F1 . i <= F1 . j
A24: ma <= len F by A1, A2, A6, Th59;
k + 1 <= ma by A1, A2, A6, Th59;
then A25: k < ma by NAT_1:13;
F1 . j = (F +* ((k + 1),(F . ma))) . j by
.= F . ma by ;
hence F1 . i <= F1 . j by A3, A10, A20, A21, A25, A24; :: thesis: verum
end;
end;
end;
end;
suppose i = j ; :: thesis: F1 . i <= F1 . j
hence F1 . i <= F1 . j ; :: thesis: verum
end;
end;
end;
end;
end;