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