let I be Program of SCM+FSA ; :: thesis: dom (Initialized I) = (dom I) \/ {(intloc 0 ),(IC SCM+FSA )}
thus dom (Initialized I) = dom (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= (dom I) \/ {(intloc 0 ),(IC SCM+FSA )} by Th40, FUNCT_4:def 1 ; :: thesis: verum