let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds
s1 = s2
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds
s1 = s2
let s1, s2 be State of S; :: thesis: ( s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) implies s1 = s2 )
s1 = s1 | ((Data-Locations ) \/ {(IC )}) by Th33;
hence ( s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) implies s1 = s2 ) by Th33; :: thesis: verum