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 program-free 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 program-free PartState of S holds NPP (p +* d) = (NPP p) +* d
let p be PartState of S; :: thesis: for d being program-free PartState of S holds NPP (p +* d) = (NPP p) +* d
let d be program-free PartState of S; :: thesis: NPP (p +* d) = (NPP p) +* d
A1: dom d misses NAT by Lm40;
A2: 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 A3: 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 A4: 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 A1, RELAT_1:95
.= d | the carrier of S
.= d by A2, RELAT_1:97 ;
hence NPP (p +* d) = (NPP p) +* d by A3, A4, FUNCT_4:75; :: thesis: verum