let p1, p2 be FinPartState of S; :: thesis: ( ( for p9 being State of S st p c= p9 holds
p1 = (Result f,p9) | (dom p) ) & ( for p9 being State of S st p c= p9 holds
p2 = (Result f,p9) | (dom p) ) implies p1 = p2 )
assume that
A8: for p9 being State of S st p c= p9 holds
p1 = (Result f,p9) | (dom p) and
A9: for p9 being State of S st p c= p9 holds
p2 = (Result f,p9) | (dom p) ; :: thesis: p1 = p2
thus p1 = (Result f,h) | (dom p) by A2, A8
.= p2 by A2, A9 ; :: thesis: verum