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