let I be Program of SCMPDS ; :: thesis: (Initialized I) | NAT = I
A1: not IC SCMPDS in NAT by AMI_1:48;
( dom I c= NAT & dom (Start-At 0 ,SCMPDS ) = {(IC SCMPDS )} ) by FUNCOP_1:19, RELAT_1:def 18;
hence (Initialized I) | NAT = I by A1, FUNCT_4:82, ZFMISC_1:56; :: thesis: verum