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