let i be Instruction of SCMPDS ; :: thesis: for I, J, K being Program of SCMPDS holds (((i ';' I) ';' J) ';' K) . 0 = i
let I, J, K be Program of SCMPDS ; :: thesis: (((i ';' I) ';' J) ';' K) . 0 = i
A1: 0 in dom (Load i) by SCMPDS_5:2;
((i ';' I) ';' J) ';' K = (i ';' (I ';' J)) ';' K by SCMPDS_4:50
.= i ';' ((I ';' J) ';' K) by SCMPDS_4:50
.= (Load i) ';' ((I ';' J) ';' K) ;
hence (((i ';' I) ';' J) ';' K) . 0 = (Load i) . 0 by A1, SCMPDS_4:37
.= i by SCMPDS_5:4 ;
:: thesis: verum