let IT1, IT2 be NAT -defined FinPartState of ; :: thesis: ( dom IT1 = dom p & ( for m being Element of NAT st m in dom p holds
IT1 . m = IncAddr (p /. m),k ) & dom IT2 = dom p & ( for m being Element of NAT st m in dom p holds
IT2 . m = IncAddr (p /. m),k ) implies IT1 = IT2 )
assume that
A8: dom IT1 = dom p and
A9: for m being Element of NAT st m in dom p holds
IT1 . m = IncAddr (p /. m),k and
A10: dom IT2 = dom p and
A11: for m being Element of NAT st m in dom p holds
IT2 . m = IncAddr (p /. m),k ; :: thesis: IT1 = IT2
for x being set st x in dom p holds
IT1 . x = IT2 . x

proof

let x be set ; :: thesis: ( x in dom p implies IT1 . x = IT2 . x )
assume A12: x in dom p ; :: thesis: IT1 . x = IT2 . x
dom p c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A12;
reconsider m = l as Element of NAT ;
thus IT1 . x = IncAddr (p /. m),k by A9, A12
.= IT2 . x by A11, A12 ; :: thesis: verum

end;

hence IT1 = IT2 by A8, A10, FUNCT_1:9; :: thesis: verum