let i be Instruction of SCMPDS; :: thesis: ( (stop (Load i)) . 0 = i & (stop (Load i)) . 1 = halt SCMPDS )
set II = Load i;
0 in dom (Load i) by Th5;
hence (stop (Load i)) . 0 = (Load i) . 0 by AFINSQ_1:def 4
.= i by FUNCOP_1:87 ;
:: thesis: (stop (Load i)) . 1 = halt SCMPDS
y: 0 in dom (Stop SCMPDS) by COMPOS_1:45;
x: (Stop SCMPDS) . 0 = halt SCMPDS by AFINSQ_1:38;
1 = 0 + (card (Load i)) by Th6;
hence (stop (Load i)) . 1 = halt SCMPDS by x, y, AFINSQ_1:def 4; :: thesis: verum