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 A5, FUNCT_7:30;

A8: dom (F +* ((k + 1),(F . ma))) = dom F by FUNCT_7:30;

then A9: k + 1 in dom F1 by A1, A7, A6, FINSEQ_3:25;

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 A1, A12, XXREAL_0:2;

1 <= j by A10, A11, XXREAL_0:2;

then A14: j in dom F1 by A7, A8, A13, FINSEQ_3:25;

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 A5, FUNCT_7:30;

A8: dom (F +* ((k + 1),(F . ma))) = dom F by FUNCT_7:30;

then A9: k + 1 in dom F1 by A1, A7, A6, FINSEQ_3:25;

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 A1, A12, XXREAL_0:2;

1 <= j by A10, A11, XXREAL_0:2;

then A14: j in dom F1 by A7, A8, A13, FINSEQ_3:25;

per cases
( j < k + 1 or j = k + 1 )
by A12, XXREAL_0:1;

end;

suppose A15:
j < k + 1
; :: thesis: F1 . i <= F1 . j

then
i < k + 1
by A11, XXREAL_0:2;

then i <> ma by A1, A2, A6, Th59;

then A16: F1 . i = (F +* ((k + 1),(F . ma))) . i by A5, FUNCT_7:32

.= F . i by A11, A15, FUNCT_7:32 ;

j <> ma by A1, A2, A6, A15, Th59;

then A17: F1 . j = (F +* ((k + 1),(F . ma))) . j by A5, FUNCT_7:32

.= F . j by A15, FUNCT_7:32 ;

j <= k by A15, NAT_1:13;

hence F1 . i <= F1 . j by A4, A10, A11, A16, A17; :: thesis: verum

end;then i <> ma by A1, A2, A6, Th59;

then A16: F1 . i = (F +* ((k + 1),(F . ma))) . i by A5, FUNCT_7:32

.= F . i by A11, A15, FUNCT_7:32 ;

j <> ma by A1, A2, A6, A15, Th59;

then A17: F1 . j = (F +* ((k + 1),(F . ma))) . j by A5, FUNCT_7:32

.= F . j by A15, FUNCT_7:32 ;

j <= k by A15, NAT_1:13;

hence F1 . i <= F1 . j by A4, A10, A11, A16, A17; :: thesis: verum

suppose A18:
j = k + 1
; :: thesis: F1 . i <= F1 . j

thus
F1 . i <= F1 . j
:: thesis: verum

end;proof
end;

per cases
( i < j or i = j )
by A11, XXREAL_0:1;

end;

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 A5, FUNCT_7:32

.= F . i by A18, A19, FUNCT_7:32 ;

A21: i <= k by A18, A19, NAT_1:13;

A22: k < j by A18, NAT_1:13;

thus F1 . i <= F1 . j :: thesis: verum

end;then A20: F1 . i = (F +* ((k + 1),(F . ma))) . i by A5, FUNCT_7:32

.= F . i by A18, A19, FUNCT_7:32 ;

A21: i <= k by A18, A19, NAT_1:13;

A22: k < j by A18, NAT_1:13;

thus F1 . i <= F1 . j :: thesis: verum

proof
end;

per cases
( k + 1 = ma or k + 1 <> ma )
;

end;

suppose
k + 1 = ma
; :: thesis: F1 . i <= F1 . j

then
F1 . j = F . (k + 1)
by A5, A7, A9, A18, FUNCT_7:31;

hence F1 . i <= F1 . j by A1, A3, A10, A18, A20, A21, A22; :: thesis: verum

end;hence F1 . i <= F1 . j by A1, A3, A10, A18, A20, A21, A22; :: thesis: verum

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 A5, A18, A23, FUNCT_7:32

.= F . ma by A7, A8, A14, A18, FUNCT_7:31 ;

hence F1 . i <= F1 . j by A3, A10, A20, A21, A25, A24; :: thesis: verum

end;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 A5, A18, A23, FUNCT_7:32

.= F . ma by A7, A8, A14, A18, FUNCT_7:31 ;

hence F1 . i <= F1 . j by A3, A10, A20, A21, A25, A24; :: thesis: verum