set T1 = {(IC )};

set T2 = SCM-Data-Loc ;

set T3 = NAT ;

let s1, s2 be State of SCMPDS; :: thesis: ( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )

s1 . x = s2 . x ) implies for a being Int_position holds s1 . a = s2 . a ) by AMI_2:def 16;

A4: dom s2 = the carrier of SCMPDS by PARTFUN1:def 2;

dom s1 = the carrier of SCMPDS by PARTFUN1:def 2;

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

set T2 = SCM-Data-Loc ;

set T3 = NAT ;

let s1, s2 be State of SCMPDS; :: thesis: ( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )

A1: now :: thesis: ( ( for a being Int_position holds s1 . a = s2 . a ) implies for x being set st x in SCM-Data-Loc holds

s1 . x = s2 . x )

A3:
( ( for x being set st x in SCM-Data-Loc holds s1 . x = s2 . x )

assume A2:
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

end;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 AMI_2:def 16;

hence s1 . x = s2 . x by A2; :: thesis: verum

end;assume x in SCM-Data-Loc ; :: thesis: s1 . x = s2 . x

then x is Int_position by AMI_2:def 16;

hence s1 . x = s2 . x by A2; :: thesis: verum

s1 . x = s2 . x ) implies for a being Int_position holds s1 . a = s2 . a ) by AMI_2:def 16;

A4: dom s2 = the carrier of SCMPDS by PARTFUN1:def 2;

dom s1 = the carrier of SCMPDS by PARTFUN1:def 2;

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