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 s being State of S
for p being NAT -defined PartState of holds NPP s = NPP (s +* p)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S
for p being NAT -defined PartState of holds NPP s = NPP (s +* p)
let s be State of S; :: thesis: for p being NAT -defined PartState of holds NPP s = NPP (s +* p)
let p be NAT -defined PartState of ; :: thesis: NPP s = NPP (s +* p)
thus NPP s = (NPP s) +* {} by FUNCT_4:22
.= (NPP s) +* (NPP p)
.= NPP (s +* p) by Th221 ; :: thesis: verum