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 0 -started PartState of S holds Initialize p = p
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being 0 -started PartState of S holds Initialize p = p
let p be 0 -started PartState of S; :: thesis: Initialize p = p
( IC S in dom p & IC p = 0 ) by Def41;
then Start-At (0,S) c= p by FUNCT_4:90;
hence Initialize p = p by FUNCT_4:79; :: thesis: verum