let i be Instruction of SCMPDS ; :: thesis: inspos 0 in dom (Load i)
dom (Load i) = {(inspos 0 )} by FUNCOP_1:19;
hence inspos 0 in dom (Load i) by TARSKI:def 1; :: thesis: verum