let i be Instruction of ; :: thesis: for I, J, K being Program of holds (((i ';' I) ';' J) ';' K) . (inspos 0 ) = i
let I, J, K be Program of ; :: thesis: (((i ';' I) ';' J) ';' K) . (inspos 0 ) = i
A1: inspos 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) by SCMPDS_4:def 4 ;
hence (((i ';' I) ';' J) ';' K) . (inspos 0 ) = (Load i) . (inspos 0 ) by A1, SCMPDS_4:37
.= i by SCMPDS_5:4 ;
:: thesis: verum