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