let IT1, IT2 be NAT -defined the InstructionsF of S -valued finite Function; :: thesis:
assume that
A9: dom IT1 = dom p and
A10: for m being Nat st m in dom p holds
IT1 . m = IncAddr ((p /. m),k) and
A11: dom IT2 = dom p and
A12: for m being Nat st m in dom p holds
IT2 . m = IncAddr ((p /. m),k) ; :: thesis:
for x being object st x in dom p holds
IT1 . x = IT2 . x

let x be object ; :: thesis:
assume A13: x in dom p ; :: thesis:
then reconsider l = x as Element of NAT by A1;
consider m being Nat such that
A14: l = m ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
thus IT1 . x = IncAddr ((p /. m),k) by A10, A13, A14
.= IT2 . x by A12, A13, A14 ; :: thesis:

end;