let i be Instruction of SCMPDS; :: thesis: for I being Program of holds (i ';' I) . 0 = i
let I be Program of ; :: thesis: (i ';' I) . 0 = i
( i ';' I = (Load i) ';' I & 0 in dom (Load i) ) by COMPOS_1:50;
hence (i ';' I) . 0 = (Load i) . 0 by AFINSQ_1:def 3
.= i ;
:: thesis: verum