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