let F, F1 be FinSequence of INT ; :: thesis: for k, ma being Element of 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 Element of 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:32;
A6: k < k + 1 by NAT_1:13;
A7: 1 <= k + 1 by NAT_1:12;
let i, j be Element of NAT ; :: according to GRAPH_2:def 14 :: 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:32;
then A14: len F1 = len F by A5, FINSEQ_3:31;
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:27;
1 <= j by A10, NAT_1:12;
then A17: j in dom F1 by A11, FINSEQ_3:27;

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

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

then i <> ma by A1, A2, A7, Th63;
then A19: F1 . i = (F +* (k + 1),(F . ma)) . i by A4, FUNCT_7:34
.= F . i by A18, FUNCT_7:34 ;
A20: i <= k by A18, NAT_1:13;
thus F1 . i <= F1 . j :: thesis: verum

proof

per cases ( j <> ma or j = ma ) ;

suppose j <> ma ; :: thesis: F1 . i <= F1 . j

then F1 . j = (F +* (k + 1),(F . ma)) . j by A4, FUNCT_7:34
.= F . j by A10, FUNCT_7:34 ;
hence F1 . i <= F1 . j by A3, A14, A8, A11, A12, A20, A19, Def14; :: thesis: verum

end;

suppose j = ma ; :: thesis: F1 . i <= F1 . j

then F1 . j = F . (k + 1) by A4, A5, A17, FUNCT_7:33;
hence F1 . i <= F1 . j by A3, A6, A8, A15, A20, A19, Def14; :: thesis: verum

end;

end;

end;

end;

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

A22: F1 . i = F . ma

proof

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

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

hence F1 . i = F . ma by A4, A5, A16, A21, FUNCT_7:33; :: thesis: verum

end;

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

hence F1 . i = (F +* (k + 1),(F . ma)) . i by A4, A21, FUNCT_7:34
.= F . ma by A5, A13, A16, A21, FUNCT_7:33 ;
:: thesis: verum

end;

end;

end;

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

proof

per cases ( j = ma or j <> ma ) ;

suppose j = ma ; :: thesis: F1 . i <= F1 . j

then F1 . j = F . (k + 1) by A4, A5, A17, FUNCT_7:33;
hence F1 . i <= F1 . j by A1, A2, A7, A22, Th63; :: thesis: verum

end;

suppose j <> ma ; :: thesis: F1 . i <= F1 . j

then F1 . j = (F +* (k + 1),(F . ma)) . j by A4, FUNCT_7:34
.= F . j by A10, FUNCT_7:34 ;
hence F1 . i <= F1 . j by A1, A2, A14, A7, A10, A11, A22, Th63; :: thesis: verum

end;

end;

end;

end;

end;