consider h being State of S such that
A11: d c= h by PBOOLE:141;
consider H being Instruction-Sequence of S such that
A12: p c= H by PBOOLE:145;
let p1, p2 be FinPartState of S; :: thesis: ( ( for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
p1 = (Result (P,s)) | (dom d) ) & ( for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
p2 = (Result (P,s)) | (dom d) ) implies p1 = p2 )
assume that
A13: for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
p1 = (Result (P,s)) | (dom d) and
A14: for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
p2 = (Result (P,s)) | (dom d) ; :: thesis: p1 = p2
thus p1 = (Result (H,h)) | (dom d) by A13, A11, A12
.= p2 by A14, A11, A12 ; :: thesis: verum