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