let I be Program of SCMPDS ; :: thesis: I c= Initialized I
set A = NAT ;
A1: dom I c= NAT by RELAT_1:def 18;

A2: now

assume IC SCMPDS in dom I ; :: thesis: contradiction
then reconsider l = IC SCMPDS as Instruction-Location of SCMPDS by A1, AMI_1:def 4;
l = IC SCMPDS ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

dom (Start-At (inspos 0 )) = {(IC SCMPDS )} by FUNCOP_1:19;
then dom I misses dom (Start-At (inspos 0 )) by A2, ZFMISC_1:56;
hence I c= Initialized I by FUNCT_4:33; :: thesis: verum