let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of N
for s1, s2 being State of S st DataPart s1 = DataPart s2 holds
Initialize s1 = Initialize s2
let S be non empty IC-Ins-separated Mem-Struct of 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;
A4: ( 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 A4, Th78; :: thesis: verum