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