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