set A = NAT ;
let s1, s2 be State of SCMPDS; :: thesis: ( IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) implies s1,s2 equal_outside NAT )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int_position holds s1 . a = s2 . a ; :: thesis: s1,s2 equal_outside NAT
not IC SCMPDS in NAT by COMPOS_1:3;
then {(IC SCMPDS)} misses NAT by ZFMISC_1:56;
then A3: {(IC SCMPDS)} \/ SCM-Data-Loc misses NAT by AMI_2:29, XBOOLE_1:70;
A4: the carrier of SCMPDS \ NAT = ({(IC SCMPDS)} \/ SCM-Data-Loc) \ NAT by SCMPDS_3:5, XBOOLE_1:40
.= {(IC SCMPDS)} \/ SCM-Data-Loc by A3, XBOOLE_1:83 ;
A5: dom (s2 | ((dom s2) \ NAT)) = (dom s2) /\ ((dom s2) \ NAT) by RELAT_1:90
.= (dom s2) \ NAT by XBOOLE_1:28
.= {(IC SCMPDS)} \/ SCM-Data-Loc by A4, PARTFUN1:def 4 ;
A6: dom (s1 | ((dom s1) \ NAT)) = (dom s1) /\ ((dom s1) \ NAT) by RELAT_1:90
.= (dom s1) \ NAT by XBOOLE_1:28
.= {(IC SCMPDS)} \/ SCM-Data-Loc by A4, PARTFUN1:def 4 ;

now

let x be set ; :: thesis: ( x in {(IC SCMPDS)} \/ SCM-Data-Loc implies (s1 | ((dom s1) \ NAT)) . b₁ = (s2 | ((dom s2) \ NAT)) . b₁ )
assume A7: x in {(IC SCMPDS)} \/ SCM-Data-Loc ; :: thesis: (s1 | ((dom s1) \ NAT)) . b₁ = (s2 | ((dom s2) \ NAT)) . b₁

per cases ( x in {(IC SCMPDS)} or x in SCM-Data-Loc ) by A7, XBOOLE_0:def 3;

suppose x in {(IC SCMPDS)} ; :: thesis: (s1 | ((dom s1) \ NAT)) . b₁ = (s2 | ((dom s2) \ NAT)) . b₁

then A8: x = IC SCMPDS by TARSKI:def 1;
hence (s1 | ((dom s1) \ NAT)) . x = IC s1 by A6, A7, FUNCT_1:70
.= (s2 | ((dom s2) \ NAT)) . x by A1, A5, A7, A8, FUNCT_1:70 ;
:: thesis: verum

end;

suppose x in SCM-Data-Loc ; :: thesis: (s1 | ((dom s1) \ NAT)) . b₁ = (s2 | ((dom s2) \ NAT)) . b₁

then A9: x is Int_position by SCMPDS_2:9;
thus (s1 | ((dom s1) \ NAT)) . x = s1 . x by A6, A7, FUNCT_1:70
.= s2 . x by A2, A9
.= (s2 | ((dom s2) \ NAT)) . x by A5, A7, FUNCT_1:70 ; :: thesis: verum

end;

end;

end;

hence s1 | ((dom s1) \ NAT) = s2 | ((dom s2) \ NAT) by A6, A5, FUNCT_1:9; :: according to FUNCT_7:def 2 :: thesis: verum