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