A: dom (Initialize ((intloc 0) .--> 1)) = (dom (Start-At (0,SCM+FSA))) \/ (dom ((intloc 0) .--> 1)) by FUNCT_4:def 1;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def 1;
hence intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by A, XBOOLE_0:def 3; :: thesis: verum