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