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 NAT -defined the Instructions of b₁ -valued Function
for p being PartState of S holds NPP (p +* P) = NPP p
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for P being NAT -defined the Instructions of S -valued Function
for p being PartState of S holds NPP (p +* P) = NPP p
let P be NAT -defined the Instructions of S -valued Function; :: thesis: for p being PartState of S holds NPP (p +* P) = NPP p
let p be PartState of S; :: thesis: NPP (p +* P) = NPP p
A: P | NAT = P by RELAT_1:209;
C: NAT misses the carrier of S \ NAT by XBOOLE_1:79;
B: NPP p = p | ( the carrier of S \ NAT) by Th65;
NPP (p +* P) = (p +* P) | ( the carrier of S \ NAT) by Th65;
hence NPP (p +* P) = (NPP p) +* (P | ( the carrier of S \ NAT)) by B, FUNCT_4:75
.= (NPP p) +* {} by A, C, RELAT_1:207
.= NPP p by FUNCT_4:22 ;
:: thesis: verum