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 & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_split_at 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 & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) implies F1 is_split_at 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: F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) ; :: thesis: F1 is_split_at k + 1

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

A6: k < k + 1 by NAT_1:13;

A7: 1 <= k + 1 by NAT_1:12;

let i, j be Nat; :: according to FINSEQ_6:def 10 :: thesis: ( 1 <= i & i <= k + 1 & k + 1 < j & j <= len F1 implies F1 . i <= F1 . j )

assume that

A8: 1 <= i and

A9: i <= k + 1 and

A10: k + 1 < j and

A11: j <= len F1 ; :: thesis: F1 . i <= F1 . j

A12: k < j by A10, NAT_1:13;

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

then A14: len F1 = len F by A5, FINSEQ_3:29;

then A15: k + 1 <= len F by A10, A11, XXREAL_0:2;

i <= len F1 by A1, A14, A9, XXREAL_0:2;

then A16: i in dom F1 by A8, FINSEQ_3:25;

1 <= j by A10, NAT_1:12;

then A17: j in dom F1 by A11, FINSEQ_3:25;

F1 is_split_at 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 & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) implies F1 is_split_at 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: F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) ; :: thesis: F1 is_split_at k + 1

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

A6: k < k + 1 by NAT_1:13;

A7: 1 <= k + 1 by NAT_1:12;

let i, j be Nat; :: according to FINSEQ_6:def 10 :: thesis: ( 1 <= i & i <= k + 1 & k + 1 < j & j <= len F1 implies F1 . i <= F1 . j )

assume that

A8: 1 <= i and

A9: i <= k + 1 and

A10: k + 1 < j and

A11: j <= len F1 ; :: thesis: F1 . i <= F1 . j

A12: k < j by A10, NAT_1:13;

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

then A14: len F1 = len F by A5, FINSEQ_3:29;

then A15: k + 1 <= len F by A10, A11, XXREAL_0:2;

i <= len F1 by A1, A14, A9, XXREAL_0:2;

then A16: i in dom F1 by A8, FINSEQ_3:25;

1 <= j by A10, NAT_1:12;

then A17: j in dom F1 by A11, FINSEQ_3:25;

per cases
( i < k + 1 or i = k + 1 )
by A9, XXREAL_0:1;

end;

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

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

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

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

A20: i <= k by A18, NAT_1:13;

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

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

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

A20: i <= k by A18, NAT_1:13;

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

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

A22:
F1 . i = F . ma

end;proof end;

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