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