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 DataPart s1 = DataPart s2 holds
Initialize s1 = Initialize 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 DataPart s1 = DataPart s2 holds
Initialize s1 = Initialize s2
let s1, s2 be State of S; :: thesis: ( DataPart s1 = DataPart s2 implies Initialize s1 = Initialize s2 )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: Initialize s1 = Initialize s2
set S1 = Initialize s1;
set S2 = Initialize s2;
A2: ( IC (Initialize s1) = 0 & IC (Initialize s2) = 0 ) by Th47;
DataPart (Initialize s1) = DataPart s1 by Th45
.= DataPart (Initialize s2) by A1, Th45 ;
hence Initialize s1 = Initialize s2 by A2, Th78; :: thesis: verum