theorem Th7: :: SCMPDS_4:8

for s1, s2 being State of SCMPDS holds
( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )