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 p being PartState of S
for d being data-only PartState of S holds NPP (p +* d) = (NPP p) +* d
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S
for d being data-only PartState of S holds NPP (p +* d) = (NPP p) +* d
let p be PartState of S; :: thesis: for d being data-only PartState of S holds NPP (p +* d) = (NPP p) +* d
let d be data-only PartState of S; :: thesis: NPP (p +* d) = (NPP p) +* d
X: dom d misses NAT by Th155;
Y: dom d c= the carrier of S by RELAT_1:def 18;
dom p c= the carrier of S by RELAT_1:def 18;
then X1: NPP p = p | (the carrier of S \ NAT ) by RELAT_1:211;
dom (p +* d) c= the carrier of S by RELAT_1:def 18;
then X2: NPP (p +* d) = (p +* d) | (the carrier of S \ NAT ) by RELAT_1:211;
d | (the carrier of S \ NAT ) = (d | the carrier of S) \ (d | NAT ) by RELAT_1:109
.= (d | the carrier of S) \ {} by X, RELAT_1:95
.= d | the carrier of S
.= d by Y, RELAT_1:97 ;
hence NPP (p +* d) = (NPP p) +* d by X1, X2, FUNCT_4:75; :: thesis: verum