let k be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for I being Instruction of S st I is ins-loc-free holds
IncAddr I,k = I
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for I being Instruction of S st I is ins-loc-free holds
IncAddr I,k = I
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for I being Instruction of S st I is ins-loc-free holds
IncAddr I,k = I
let I be Instruction of S; :: thesis: ( I is ins-loc-free implies IncAddr I,k = I )
assume A1: for x being set st x in dom (AddressPart I) holds
(product" (AddressParts (InsCode I))) . x <> NAT ; :: according to AMISTD_2:def 12 :: thesis: IncAddr I,k = I
set f = IncAddr I,k;
A2: InsCode (IncAddr I,k) = InsCode I by Def14;
A3: dom (AddressPart (IncAddr I,k)) = dom (AddressPart I) by Def14;
for x being set st x in dom (AddressPart I) holds
(AddressPart (IncAddr I,k)) . x = (AddressPart I) . x

proof

let x be set ; :: thesis: ( x in dom (AddressPart I) implies (AddressPart (IncAddr I,k)) . x = (AddressPart I) . x )
assume A4: x in dom (AddressPart I) ; :: thesis: (AddressPart (IncAddr I,k)) . x = (AddressPart I) . x
( (product" (AddressParts (InsCode I))) . x = NAT or (product" (AddressParts (InsCode I))) . x <> NAT ) ;
hence (AddressPart (IncAddr I,k)) . x = (AddressPart I) . x by A1, A4, Def14; :: thesis: verum

end;

hence IncAddr I,k = I by A2, Th16, A3, FUNCT_1:9; :: thesis: verum