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