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 s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (s1 +* p) = NPP (s2 +* p)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S
for s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (s1 +* p) = NPP (s2 +* p)
let p be PartState of S; :: thesis: for s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (s1 +* p) = NPP (s2 +* p)
let s1, s2 be State of S; :: thesis: ( NPP s1 = NPP s2 implies NPP (s1 +* p) = NPP (s2 +* p) )
assume NPP s1 = NPP s2 ; :: thesis: NPP (s1 +* p) = NPP (s2 +* p)
hence NPP (s1 +* p) = (NPP s2) +* (NPP p) by Th221
.= NPP (s2 +* p) by Th221 ;
:: thesis: verum