let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC S)}
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC S)}
let p be PartState of S; :: thesis: dom (Initialize p) = (dom p) \/ {(IC S)}
thus dom (Initialize p) = (dom p) \/ (dom (Start-At (0,S))) by FUNCT_4:def 1
.= (dom p) \/ {(IC S)} by FUNCOP_1:19 ; :: thesis: verum