let x be set ; :: according to AMI_1:def 29 :: thesis: ( not x in dom Sorting-Function or ex b₁ being Element of sproduct the Object-Kind of SCM+FSA st
( x = b₁ & (Initialized Insert-Sort-Algorithm ) +* b₁ is Element of sproduct the Object-Kind of SCM+FSA & Sorting-Function . b₁ c= Result ((Initialized Insert-Sort-Algorithm ) +* b₁) ) )
assume x in dom Sorting-Function ; :: thesis: ex b₁ being Element of sproduct the Object-Kind of SCM+FSA st
( x = b₁ & (Initialized Insert-Sort-Algorithm ) +* b₁ is Element of sproduct the Object-Kind of SCM+FSA & Sorting-Function . b₁ c= Result ((Initialized Insert-Sort-Algorithm ) +* b₁) )
then consider w being FinSequence of INT such that
A1: x = (fsloc 0 ) .--> w by SCMBSORT:60;
reconsider s = x as FinPartState of SCM+FSA by A1;
set p = Initialized Insert-Sort-Algorithm ;
A2: dom s = {(fsloc 0 )} by A1, FUNCOP_1:19;
take s ; :: thesis: ( x = s & (Initialized Insert-Sort-Algorithm ) +* s is Element of sproduct the Object-Kind of SCM+FSA & Sorting-Function . s c= Result ((Initialized Insert-Sort-Algorithm ) +* s) )
thus x = s ; :: thesis: ( (Initialized Insert-Sort-Algorithm ) +* s is Element of sproduct the Object-Kind of SCM+FSA & Sorting-Function . s c= Result ((Initialized Insert-Sort-Algorithm ) +* s) )
A3: (Initialized Insert-Sort-Algorithm ) +* s is autonomic by A1, Th48;
A4: dom (Initialized Insert-Sort-Algorithm ) misses dom s by A1, SCMBSORT:46;

A5: now

let t be State of SCM+FSA ; :: thesis: ( (Initialized Insert-Sort-Algorithm ) +* s c= t implies t is halting )
assume A6: (Initialized Insert-Sort-Algorithm ) +* s c= t ; :: thesis: t is halting
set bf = insert-sort (fsloc 0 );
Initialized Insert-Sort-Algorithm c= (Initialized Insert-Sort-Algorithm ) +* s by A4, FUNCT_4:33;
then A7: Initialized Insert-Sort-Algorithm c= t by A6, XBOOLE_1:1;
Initialized (insert-sort (fsloc 0 )) is halting by Th44;
hence t is halting by A7, AMI_1:def 26; :: thesis: verum

end;

then A8: (Initialized Insert-Sort-Algorithm ) +* s is halting by AMI_1:def 26;
thus (Initialized Insert-Sort-Algorithm ) +* s is pre-program of SCM+FSA by A1, A5, Th48, AMI_1:def 26; :: thesis: Sorting-Function . s c= Result ((Initialized Insert-Sort-Algorithm ) +* s)
consider z being FinSequence of REAL such that
A9: ( w,z are_fiberwise_equipotent & z is non-increasing & z is FinSequence of INT & Sorting-Function . s = (fsloc 0 ) .--> z ) by A1, SCMBSORT:61;
consider t being State of SCM+FSA such that
A10: (Initialized Insert-Sort-Algorithm ) +* s c= t by CARD_3:97;
consider u being FinSequence of REAL such that
A11: ( w,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result t) . (fsloc 0 ) = u ) by A1, A10, Th47;
A12: u = z by A9, A11, CLASSES1:84, RFINSEQ:36;
fsloc 0 in the carrier of SCM+FSA ;
then A13: fsloc 0 in dom (Result t) by AMI_1:79;
s c= (Initialized Insert-Sort-Algorithm ) +* s by FUNCT_4:26;
then A14: dom s c= dom ((Initialized Insert-Sort-Algorithm ) +* s) by RELAT_1:25;
A15: dom ((fsloc 0 ) .--> z) = {(fsloc 0 )} by FUNCOP_1:19;
Result ((Initialized Insert-Sort-Algorithm ) +* s) = (Result t) | (dom ((Initialized Insert-Sort-Algorithm ) +* s)) by A3, A8, A10, AMI_1:def 28;
hence Sorting-Function . s c= Result ((Initialized Insert-Sort-Algorithm ) +* s) by A2, A9, A11, A12, A13, A14, A15, FUNCT_4:90, RELAT_1:186; :: thesis: verum