consider h being State of S such that
A12: d c= h by PBOOLE:156;
let p1, p2 be FinPartState of S; :: thesis: ( ( for s being State of S st d c= s holds
p1 = (Result ((ProgramPart s),s)) | (dom (NPP d)) ) & ( for s being State of S st d c= s holds
p2 = (Result ((ProgramPart s),s)) | (dom (NPP d)) ) implies p1 = p2 )
assume that
A13: for s being State of S st d c= s holds
p1 = (Result ((ProgramPart s),s)) | (dom (NPP d)) and
A14: for s being State of S st d c= s holds
p2 = (Result ((ProgramPart s),s)) | (dom (NPP d)) ; :: thesis: p1 = p2
thus p1 = (Result ((ProgramPart h),h)) | (dom (NPP d)) by A13, A12
.= p2 by A14, A12 ; :: thesis: verum