consider h being State of S such that
A12: d c= h by PBOOLE:156;
B12: ProgramPart d c= ProgramPart h by A12, RELAT_1:105;
let p1, p2 be FinPartState of S; :: thesis: ( ( for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
p1 = (Result (P,s)) | (dom (NPP d)) ) & ( for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
p2 = (Result (P,s)) | (dom (NPP d)) ) implies p1 = p2 )
assume that
A13: for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
p1 = (Result (P,s)) | (dom (NPP d)) and
A14: for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
p2 = (Result (P,s)) | (dom (NPP d)) ; :: thesis: p1 = p2
thus p1 = (Result ((ProgramPart h),h)) | (dom (NPP d)) by A1, A13, A12, B12
.= p2 by A1, A14, A12, B12 ; :: thesis: verum