let s1, s2 be State of SCMPDS ; :: thesis: ( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )
set T1 = {(IC SCMPDS )};
set T2 = SCM-Data-Loc ;
set T3 = NAT ;
A1: ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT = SCM-Data-Loc \/ ({(IC SCMPDS )} \/ NAT ) by XBOOLE_1:4;
dom s1 = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, SCMPDS_3:5;
then A2: SCM-Data-Loc c= dom s1 by A1, XBOOLE_1:7;
dom s2 = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, SCMPDS_3:5;
then A3: SCM-Data-Loc c= dom s2 by A1, XBOOLE_1:7;

A4: now

assume A5: for a being Int_position holds s1 . a = s2 . a ; :: thesis: for x being set st x in SCM-Data-Loc holds
s1 . x = s2 . x

hereby :: thesis: verum

let x be set ; :: thesis: ( x in SCM-Data-Loc implies s1 . x = s2 . x )
assume x in SCM-Data-Loc ; :: thesis: s1 . x = s2 . x
then x is Int_position by SCMPDS_2:9;
hence s1 . x = s2 . x by A5; :: thesis: verum

end;

end;

now

assume A6: for x being set st x in SCM-Data-Loc holds
s1 . x = s2 . x ; :: thesis: for a being Int_position holds s1 . a = s2 . a

hereby :: thesis: verum

let a be Int_position ; :: thesis: s1 . a = s2 . a
a in SCM-Data-Loc by SCMPDS_2:def 2;
hence s1 . a = s2 . a by A6; :: thesis: verum

end;

end;

hence ( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 ) by A2, A3, A4, FUNCT_1:165, SCMPDS_2:100; :: thesis: verum