let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of N
for p being 0 -started PartState of S holds Initialize p = p
let S be non empty IC-Ins-separated Mem-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 in dom p & IC p = 0 ) by Def16;
hence Initialize p = p by FUNCT_4:85, FUNCT_4:98; :: thesis: verum