let s1, s2 be State of SCMPDS; :: thesis: ( ( for a being Int_position holds s1 . a = s2 . a ) implies Initialize s1 = Initialize s2 )
assume for a being Int_position holds s1 . a = s2 . a ; :: thesis: Initialize s1 = Initialize s2
then DataPart s1 = DataPart s2 by SCMPDS_4:8;
hence Initialize s1 = Initialize s2 by MEMSTR_0:80; :: thesis: verum