set A = NAT ;
let s1, s2 be State of SCM+FSA; :: thesis: ( IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies NPP s1 = NPP s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int-Location holds s1 . a = s2 . a and
A3: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: NPP s1 = NPP s2
not IC in NAT by COMPOS_1:3;
then ( Data-Locations SCM+FSA misses NAT & {(IC )} misses NAT ) by ZFMISC_1:56, COMPOS_1:51;
then A4: (Data-Locations SCM+FSA) \/ {(IC )} misses NAT by XBOOLE_1:70;
the carrier of SCM+FSA = ({(IC )} \/ (Data-Locations SCM+FSA)) \/ NAT by COMPOS_1:160;
then A5: the carrier of SCM+FSA \ NAT = ((Data-Locations SCM+FSA) \/ {(IC )}) \ NAT by XBOOLE_1:40
.= (Data-Locations SCM+FSA) \/ {(IC )} by A4, XBOOLE_1:83 ;
A6: dom (s2 | ((dom s2) \ NAT)) = (dom s2) /\ ((dom s2) \ NAT) by RELAT_1:90
.= (dom s2) \ NAT by XBOOLE_1:28
.= (Data-Locations SCM+FSA) \/ {(IC )} by A5, PARTFUN1:def 4 ;
A7: dom (s1 | ((dom s1) \ NAT)) = (dom s1) /\ ((dom s1) \ NAT) by RELAT_1:90
.= (dom s1) \ NAT by XBOOLE_1:28
.= (Data-Locations SCM+FSA) \/ {(IC )} by A5, PARTFUN1:def 4 ;

now

let x be set ; :: thesis: ( x in (Data-Locations SCM+FSA) \/ {(IC )} implies (s1 | ((dom s1) \ NAT)) . b₁ = (s2 | ((dom s2) \ NAT)) . b₁ )
assume A8: x in (Data-Locations SCM+FSA) \/ {(IC )} ; :: thesis: (s1 | ((dom s1) \ NAT)) . b₁ = (s2 | ((dom s2) \ NAT)) . b₁
then A9: ( x in Data-Locations SCM+FSA or x in {(IC )} ) by XBOOLE_0:def 3;

per cases ( x in Int-Locations or x in FinSeq-Locations or x in {(IC )} ) by A9, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in Int-Locations ; :: thesis: (s1 | ((dom s1) \ NAT)) . b₁ = (s2 | ((dom s2) \ NAT)) . b₁

then A10: x is Int-Location by SCMFSA_2:11;
thus (s1 | ((dom s1) \ NAT)) . x = s1 . x by A7, A8, FUNCT_1:70
.= s2 . x by A2, A10
.= (s2 | ((dom s2) \ NAT)) . x by A6, A8, FUNCT_1:70 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: (s1 | ((dom s1) \ NAT)) . b₁ = (s2 | ((dom s2) \ NAT)) . b₁

then A11: x is FinSeq-Location by SCMFSA_2:12;
thus (s1 | ((dom s1) \ NAT)) . x = s1 . x by A7, A8, FUNCT_1:70
.= s2 . x by A3, A11
.= (s2 | ((dom s2) \ NAT)) . x by A6, A8, FUNCT_1:70 ; :: thesis: verum

end;

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

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

end;

end;

end;

then s1 | ((dom s1) \ NAT) = s2 | ((dom s2) \ NAT) by A7, A6, FUNCT_1:9;
hence NPP s1 = NPP s2 by COMPOS_1:233; :: thesis: verum