let s be State of SCM+FSA; :: thesis: for t being FinSequence of INT st (Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> t) c= s holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result ((ProgramPart s),s)) . (fsloc 0) = u )
let t be FinSequence of INT ; :: thesis: ( (Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> t) c= s implies ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result ((ProgramPart s),s)) . (fsloc 0) = u ) )
set Ia = Insert-Sort-Algorithm ;
set p = Initialized Insert-Sort-Algorithm;
set x = (fsloc 0) .--> t;
set z = (IExec ((insert-sort (fsloc 0)),s)) . (fsloc 0);
assume A1: (Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> t) c= s ; :: thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result ((ProgramPart s),s)) . (fsloc 0) = u )
reconsider u = (IExec ((insert-sort (fsloc 0)),s)) . (fsloc 0) as FinSequence of REAL by FINSEQ_3:126;
take u ; :: thesis: ( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result ((ProgramPart s),s)) . (fsloc 0) = u )
dom ((fsloc 0) .--> t) = {(fsloc 0)} by FUNCOP_1:19;
then A2: fsloc 0 in dom ((fsloc 0) .--> t) by TARSKI:def 1;
then fsloc 0 in dom ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> t)) by FUNCT_4:13;
then s . (fsloc 0) = ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> t)) . (fsloc 0) by A1, GRFUNC_1:8
.= ((fsloc 0) .--> t) . (fsloc 0) by A2, FUNCT_4:14
.= t by FUNCOP_1:87 ;
hence t,u are_fiberwise_equipotent by Th45; :: thesis: ( u is non-increasing & u is FinSequence of INT & (Result ((ProgramPart s),s)) . (fsloc 0) = u )
s . (fsloc 0),(IExec ((insert-sort (fsloc 0)),s)) . (fsloc 0) are_fiberwise_equipotent by Th45;
then A3: dom (s . (fsloc 0)) = dom u by RFINSEQ:16;

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
A4: i in dom u and
A5: j in dom u and
A6: i < j ; :: thesis: u . i >= u . j
A7: i >= 1 by A4, FINSEQ_3:27;
j <= len (s . (fsloc 0)) by A3, A5, FINSEQ_3:27;
hence u . i >= u . j by A6, A7, Th45; :: thesis: verum
reconsider y2 = ((IExec ((insert-sort (fsloc 0)),s)) . (fsloc 0)) . j as Integer ;
reconsider y1 = ((IExec ((insert-sort (fsloc 0)),s)) . (fsloc 0)) . i as Integer ;

end;

hence u is non-increasing by RFINSEQ:32; :: thesis: ( u is FinSequence of INT & (Result ((ProgramPart s),s)) . (fsloc 0) = u )
thus u is FinSequence of INT ; :: thesis: (Result ((ProgramPart s),s)) . (fsloc 0) = u
dom (Initialized Insert-Sort-Algorithm) misses dom ((fsloc 0) .--> t) by SCMBSORT:46;
then Initialized Insert-Sort-Algorithm c= (Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> t) by FUNCT_4:33;
then Initialized Insert-Sort-Algorithm c= s by A1, XBOOLE_1:1;
then s = s +* (Initialized Insert-Sort-Algorithm) by FUNCT_4:79;
hence (Result ((ProgramPart s),s)) . (fsloc 0) = u by SCMBSORT:57; :: thesis: verum