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

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