let s be State of SCM+FSA; :: thesis: for t being FinSequence of INT
for P being Instruction-Sequence of SCM+FSA st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Insert-Sort-Algorithm c= P holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (P,s)) . (fsloc 0) = u )
let t be FinSequence of INT ; :: thesis: for P being Instruction-Sequence of SCM+FSA st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Insert-Sort-Algorithm c= P holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (P,s)) . (fsloc 0) = u )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Insert-Sort-Algorithm c= P implies ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (P,s)) . (fsloc 0) = u ) )
set Ia = Insert-Sort-Algorithm ;
set p = Initialize ((intloc 0) .--> 1);
set x = (fsloc 0) .--> t;
set z = (IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0);
assume that
A1: (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s and
A2: Insert-Sort-Algorithm c= P ; :: thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (P,s)) . (fsloc 0) = u )
A3: P +* Insert-Sort-Algorithm = P by A2, FUNCT_4:98;
reconsider u = (IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0) as FinSequence of REAL by FINSEQ_3:117;
take u ; :: thesis: ( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (P,s)) . (fsloc 0) = u )
DD: dom ((fsloc 0) .--> t) = {(fsloc 0)} by FUNCOP_1:13;
then A4: fsloc 0 in dom ((fsloc 0) .--> t) by TARSKI:def 1;
then fsloc 0 in dom ((Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t)) by FUNCT_4:12;
then s . (fsloc 0) = ((Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t)) . (fsloc 0) by A1, GRFUNC_1:2
.= ((fsloc 0) .--> t) . (fsloc 0) by A4, FUNCT_4:13
.= t by FUNCOP_1:72 ;
hence t,u are_fiberwise_equipotent by Th45; :: thesis: ( u is non-increasing & u is FinSequence of INT & (Result (P,s)) . (fsloc 0) = u )
s . (fsloc 0),(IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0) are_fiberwise_equipotent by Th45;
then A5: dom (s . (fsloc 0)) = dom u by RFINSEQ:3;

now

let i, j be Element of NAT ; :: thesis: ( i in dom u & j in dom u & i < j implies u . i >= u . j )
assume that
A6: i in dom u and
A7: j in dom u and
A8: i < j ; :: thesis: u . i >= u . j
A9: i >= 1 by A6, FINSEQ_3:25;
j <= len (s . (fsloc 0)) by A5, A7, FINSEQ_3:25;
hence u . i >= u . j by A8, A9, Th45; :: thesis: verum
reconsider y2 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . j as Integer ;
reconsider y1 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . i as Integer ;

end;

hence u is non-increasing by RFINSEQ:19; :: thesis: ( u is FinSequence of INT & (Result (P,s)) . (fsloc 0) = u )
thus u is FinSequence of INT ; :: thesis: (Result (P,s)) . (fsloc 0) = u
L1: dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )} by SCMFSA6A:42;
( fsloc 0 <> intloc 0 & fsloc 0 <> IC ) by SCMFSA_2:57, SCMFSA_2:58;
then not fsloc 0 in dom (Initialize ((intloc 0) .--> 1)) by L1, TARSKI:def 2;
then dom (Initialize ((intloc 0) .--> 1)) misses dom ((fsloc 0) .--> t) by DD, ZFMISC_1:50;
then Initialize ((intloc 0) .--> 1) c= (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) by FUNCT_4:32;
then XX: Initialize ((intloc 0) .--> 1) c= s by A1, XBOOLE_1:1;
Initialize ((intloc 0) .--> 1) c= s by XX;
then s = s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:98;
then E1: s = Initialized s by SCMFSA6A:def 3;
(Result ((P +* Insert-Sort-Algorithm),(Initialized s))) . (fsloc 0) = (IExec (Insert-Sort-Algorithm,P,s)) . (fsloc 0) by SCMBSORT:33;
hence (Result (P,s)) . (fsloc 0) = u by A3, E1; :: thesis: verum