A: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
C: Int-Locations misses NAT by SCMFSA_2:13;
intloc 0 in Int-Locations by SCMFSA_2:9;
then D: not intloc 0 in NAT by C, XBOOLE_0:3;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:19;
then B: dom ((intloc 0) .--> 1) misses NAT by D, ZFMISC_1:56;
dom (Start-At (0,SCM+FSA)) misses NAT by COMPOS_1:26;
hence dom (Initialize ((intloc 0) .--> 1)) misses NAT by A, B, XBOOLE_1:70; :: thesis: verum