let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st Initialize p c= s holds
IC s = 0
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for s being State of S
for p being PartState of S st Initialize p c= s holds
IC s = 0
let s be State of S; :: thesis: for p being PartState of S st Initialize p c= s holds
IC s = 0
let p be PartState of S; :: thesis: ( Initialize p c= s implies IC s = 0 )
A1: IC (Initialize p) = 0 by Def11;
A2: IC in dom (Initialize p) by Def11;
assume Initialize p c= s ; :: thesis: IC s = 0
hence IC s = 0 by A1, A2, GRFUNC_1:2; :: thesis: verum