let IT1, IT2 be FinPartState of S; :: thesis: ( dom IT1 = dom p & ( for m being natural number st il. S,m in dom p holds
IT1 . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) & dom IT2 = dom p & ( for m being natural number st il. S,m in dom p holds
IT2 . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) implies IT1 = IT2 )
assume that
A9: dom IT1 = dom p and
A10: for m being natural number st il. S,m in dom p holds
IT1 . (il. S,m) = IncAddr (pi p,(il. S,m)),k and
A11: dom IT2 = dom p and
A12: for m being natural number st il. S,m in dom p holds
IT2 . (il. S,m) = IncAddr (pi p,(il. S,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 A13: x in dom p ; :: thesis: IT1 . x = IT2 . x
then reconsider l = x as Instruction-Location of S by A1, AMI_1:def 4;
consider m being natural number such that
A14: l = il. S,m by AMISTD_1:26;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
thus IT1 . x = IncAddr (pi p,(il. S,m)),k by A10, A13, A14
.= IT2 . x by A12, A13, A14 ; :: thesis: verum

end;

hence IT1 = IT2 by A9, A11, FUNCT_1:9; :: thesis: verum