let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s1, s2 being State of S holds
( NPP s1 = NPP s2 iff s1 | ((dom s1) \ NAT) = s2 | ((dom s2) \ NAT) )
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s1, s2 being State of S holds
( NPP s1 = NPP s2 iff s1 | ((dom s1) \ NAT) = s2 | ((dom s2) \ NAT) )
let s1, s2 be State of S; :: thesis: ( NPP s1 = NPP s2 iff s1 | ((dom s1) \ NAT) = s2 | ((dom s2) \ NAT) )
A: NPP s1 = s1 | ((dom s1) \ NAT) by Th232;
NPP s2 = s2 | ((dom s2) \ NAT) by Th232;
hence ( NPP s1 = NPP s2 iff s1 | ((dom s1) \ NAT) = s2 | ((dom s2) \ NAT) ) by A; :: thesis: verum