let I be Program of SCMPDS ; :: thesis: dom (Initialized I) = (dom I) \/ {(IC SCMPDS )}
thus dom (Initialized I) = (dom I) \/ (dom (Start-At 0 ,SCMPDS )) by FUNCT_4:def 1
.= (dom I) \/ {(IC SCMPDS )} by FUNCOP_1:19 ; :: thesis: verum