consider h being State of S such that
A10: 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 d) ) & ( for s being State of S st d c= s holds
p2 = (Result ((ProgramPart s),s)) | (dom d) ) implies p1 = p2 )
assume that
A11: for s being State of S st d c= s holds
p1 = (Result ((ProgramPart s),s)) | (dom d) and
A12: for s being State of S st d c= s holds
p2 = (Result ((ProgramPart s),s)) | (dom d) ; :: thesis: p1 = p2
thus p1 = (Result ((ProgramPart h),h)) | (dom d) by A11, A10
.= p2 by A12, A10 ; :: thesis: verum