let s be State of SCM+FSA; :: thesis: for t being FinSequence of INT
for P being Instruction-Sequence of SCM+FSA st (Initialize (() .--> 1)) +* (() .--> 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)) . () = u )

let t be FinSequence of INT ; :: thesis: for P being Instruction-Sequence of SCM+FSA st (Initialize (() .--> 1)) +* (() .--> 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)) . () = u )

let P be Instruction-Sequence of SCM+FSA; :: thesis: ( (Initialize (() .--> 1)) +* (() .--> 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)) . () = u ) )

set Ia = Insert-Sort-Algorithm ;
set p = Initialize (() .--> 1);
set x = () .--> t;
set z = (IExec ((),P,s)) . ();
assume that
A1: (Initialize (() .--> 1)) +* (() .--> 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)) . () = u )

A3: P +* Insert-Sort-Algorithm = P by ;
reconsider u = (IExec ((),P,s)) . () 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)) . () = u )
A5: fsloc 0 in dom (() .--> t) by TARSKI:def 1;
then fsloc 0 in dom ((Initialize (() .--> 1)) +* (() .--> t)) by FUNCT_4:12;
then s . () = ((Initialize (() .--> 1)) +* (() .--> t)) . () by
.= (() .--> t) . () by
.= t by FUNCOP_1:72 ;
hence t,u are_fiberwise_equipotent by Th25; :: thesis: ( u is non-increasing & u is FinSequence of INT & (Result (P,s)) . () = u )
s . (),(IExec ((),P,s)) . () are_fiberwise_equipotent by Th25;
then A6: dom (s . ()) = dom u by RFINSEQ:3;
now :: thesis: for i, j being Nat st i in dom u & j in dom u & i < j holds
u . i >= u . j
let i, j be Nat; :: thesis: ( i in dom u & j in dom u & i < j implies u . i >= u . j )
assume that
A7: i in dom u and
A8: j in dom u and
A9: i < j ; :: thesis: u . i >= u . j
A10: i >= 1 by ;
j <= len (s . ()) by ;
hence u . i >= u . j by ; :: thesis: verum
reconsider y2 = ((IExec ((),P,s)) . ()) . j as Integer ;
reconsider y1 = ((IExec ((),P,s)) . ()) . i as Integer ;
end;
hence u is non-increasing by RFINSEQ:19; :: thesis: ( u is FinSequence of INT & (Result (P,s)) . () = u )
thus u is FinSequence of INT ; :: thesis: (Result (P,s)) . () = u
A11: dom (Initialize (() .--> 1)) = {(),()} by SCMFSA_M:11;
( fsloc 0 <> intloc 0 & fsloc 0 <> IC ) by ;
then not fsloc 0 in dom (Initialize (() .--> 1)) by ;
then dom (Initialize (() .--> 1)) misses dom (() .--> t) by ZFMISC_1:50;
then Initialize (() .--> 1) c= (Initialize (() .--> 1)) +* (() .--> t) by FUNCT_4:32;
then A12: Initialize (() .--> 1) c= s by ;
Initialize (() .--> 1) c= s by A12;
then s = s +* (Initialize (() .--> 1)) by FUNCT_4:98;
then A13: s = Initialized s ;
(Result (,())) . () = () . () by SCMBSORT:33;
hence (Result (P,s)) . () = u by ; :: thesis: verum