let s1, s2 be State of SCMPDS ; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 & s1 | NAT = s2 | NAT implies s1 = s2 )
assume A1: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 & s1 | NAT = s2 | NAT ) ; :: thesis: s1 = s2
A2: dom s1 = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by SCMPDS_4:19;
A3: dom s2 = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by SCMPDS_4:19;
then s1 | {(IC SCMPDS )} = s2 | {(IC SCMPDS )} by A1, A2, GRFUNC_1:90;
then s1 | ({(IC SCMPDS )} \/ SCM-Data-Loc ) = s2 | ({(IC SCMPDS )} \/ SCM-Data-Loc ) by A1, RELAT_1:185, SCMPDS_2:100;
then s1 | (({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT ) = s2 | (({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT ) by A1, RELAT_1:185;
hence s1 = s2 | (dom s2) by A2, A3, RELAT_1:97
.= s2 by RELAT_1:97 ;
:: thesis: verum