let I be Program of SCM+FSA ; :: thesis: (Initialized I) | NAT = I
A1: Initialized I = I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15;
A2: dom I c= NAT by RELAT_1:def 18;
dom ((intloc 0 ) .--> 1) = {(intloc 0 )} by FUNCOP_1:19;
then A3: dom ((intloc 0 ) .--> 1) misses NAT by Lm1, ZFMISC_1:56;
dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A4: dom (Start-At (insloc 0 )) misses NAT by Lm2, ZFMISC_1:56;
dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) = (dom ((intloc 0 ) .--> 1)) \/ (dom (Start-At (insloc 0 ))) by FUNCT_4:def 1;
then dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) misses NAT by A3, A4, XBOOLE_1:70;
hence (Initialized I) | NAT = I by A1, A2, FUNCT_4:82; :: thesis: verum