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, q being PartState of S holds NPP (p +* q) = (NPP p) +* (NPP q)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p, q being PartState of S holds NPP (p +* q) = (NPP p) +* (NPP q)
let p, q be PartState of S; :: thesis: NPP (p +* q) = (NPP p) +* (NPP q)
thus NPP (p +* q) = (p +* q) | ( the carrier of S \ NAT) by Th65
.= (p | ( the carrier of S \ NAT)) +* (q | ( the carrier of S \ NAT)) by FUNCT_4:75
.= (NPP p) +* (q | ( the carrier of S \ NAT)) by Th65
.= (NPP p) +* (NPP q) by Th65 ; :: thesis: verum