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