let i, j be Instruction of SCMPDS; :: thesis: for I being Program of SCMPDS holds
( ((i ';' j) ';' I) . 0 = i & ((i ';' j) ';' I) . 1 = j )
let I be Program of SCMPDS; :: thesis: ( ((i ';' j) ';' I) . 0 = i & ((i ';' j) ';' I) . 1 = j )
set jI = j ';' I;
A1: (i ';' j) ';' I = i ';' (j ';' I) by SCMPDS_4:16
.= (Load i) ';' (j ';' I) by SCMPDS_4:def 2 ;
0 in dom (Load i) by COMPOS_1:50;
hence ((i ';' j) ';' I) . 0 = (Load i) . 0 by A1, AFINSQ_1:def 3
.= i ;
:: thesis: ((i ';' j) ';' I) . 1 = j
A2: 0 in dom (Load j) by COMPOS_1:50;
0 < card (j ';' I) ;
then A3: ( card (Load i) = 1 & 0 in dom (j ';' I) ) by AFINSQ_1:66, COMPOS_1:54;
thus ((i ';' j) ';' I) . 1 = ((Load i) ';' (j ';' I)) . (0 + 1) by A1
.= (j ';' I) . 0 by A3, AFINSQ_1:def 3
.= ((Load j) ';' I) . 0 by SCMPDS_4:def 2
.= (Load j) . 0 by A2, AFINSQ_1:def 3
.= j ; :: thesis: verum