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