let I be Program of SCMPDS ; :: thesis: I c= Initialize I
set A = NAT ;
A2: not IC SCMPDS in dom I by COMPOS_1:3;
dom (Start-At 0 ,SCMPDS ) = {(IC SCMPDS )} by FUNCOP_1:19;
then dom I misses dom (Start-At 0 ,SCMPDS ) by A2, ZFMISC_1:56;
hence I c= Initialize I by FUNCT_4:33; :: thesis: verum