let n be Element of NAT ; :: thesis: for I being Program of holds dom I misses dom (Start-At (inspos n))
let I be Program of ; :: thesis: dom I misses dom (Start-At (inspos n))
A1: dom (Start-At (inspos n)) = {(IC SCMPDS )} by FUNCOP_1:19;
assume (dom I) /\ (dom (Start-At (inspos n))) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being set such that
A2: x in (dom I) /\ (dom (Start-At (inspos n))) by XBOOLE_0:def 1;
( x in dom I & x in dom (Start-At (inspos n)) ) by A2, XBOOLE_0:def 4;
then ( dom I c= NAT & IC SCMPDS in dom I ) by A1, RELAT_1:def 18, TARSKI:def 1;
then reconsider l = IC SCMPDS as Instruction-Location of SCMPDS by AMI_1:def 4;
l = IC SCMPDS ;
hence contradiction by AMI_1:48; :: thesis: verum