let F, F1 be 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 & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds
F1 is_split_at k + 1
let k, ma be Nat; ( 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)))
; 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; FINSEQ_6:def 10 ( 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
; 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;
suppose A21:
i = k + 1
;
F1 . i <= F1 . jA22:
F1 . i = F . ma
thus
F1 . i <= F1 . j
verumproof
per cases
( j = ma or j <> ma )
;
suppose
j <> ma
;
F1 . i <= F1 . jthen F1 . j =
(F +* ((k + 1),(F . ma))) . j
by A4, FUNCT_7:32
.=
F . j
by A10, FUNCT_7:32
;
hence
F1 . i <= F1 . j
by A1, A2, A14, A7, A10, A11, A22, Th59;
verum end; end;
end; end; end;