let IT1, IT2 be finite PartFunc of NAT ,the Instructions of SCM ; :: 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
A12: dom IT1 = dom p and
A13: for m being Element of NAT st m in dom p holds
IT1 . m = IncAddr (p /. m),k and
A14: dom IT2 = dom p and
A15: 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 A16: x in dom p ; :: thesis: IT1 . x = IT2 . x
dom p c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCM by A16, AMI_1:def 4;
reconsider m = l as Element of NAT by ORDINAL1:def 13;
thus IT1 . x = IncAddr (p /. m),k by A13, A16
.= IT2 . x by A15, A16 ; :: thesis: verum

end;

hence IT1 = IT2 by A12, A14, FUNCT_1:9; :: thesis: verum