let IT1, IT2 be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: ( dom IT1 = dom p & ( for m being Nat st m in dom p holds
IT1 . m = IncAddr ((p /. m),k) ) & dom IT2 = dom p & ( for m being Nat st m in dom p holds
IT2 . m = IncAddr ((p /. m),k) ) implies IT1 = IT2 )
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: IT1 = IT2
for x being object st x in dom p holds
IT1 . x = IT2 . x

proof

let x be object ; :: 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 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: verum

end;

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