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 holds AddressParts (InsCode I) = AddressParts (InsCode (IncAddr I,k))
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 holds AddressParts (InsCode I) = AddressParts (InsCode (IncAddr I,k))
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 holds AddressParts (InsCode I) = AddressParts (InsCode (IncAddr I,k))
let I be Instruction of S; :: thesis: AddressParts (InsCode I) = AddressParts (InsCode (IncAddr I,k))
set A = { (AddressPart J) where J is Instruction of S : InsCode I = InsCode J } ;
set B = { (AddressPart J) where J is Instruction of S : InsCode (IncAddr I,k) = InsCode J } ;
{ (AddressPart J) where J is Instruction of S : InsCode I = InsCode J } = { (AddressPart J) where J is Instruction of S : InsCode (IncAddr I,k) = InsCode J }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (AddressPart J) where J is Instruction of S : InsCode (IncAddr I,k) = InsCode J } c= { (AddressPart J) where J is Instruction of S : InsCode I = InsCode J }

let a be set ; :: thesis: ( a in { (AddressPart J) where J is Instruction of S : InsCode I = InsCode J } implies a in { (AddressPart J) where J is Instruction of S : InsCode (IncAddr I,k) = InsCode J } )
assume a in { (AddressPart J) where J is Instruction of S : InsCode I = InsCode J } ; :: thesis: a in { (AddressPart J) where J is Instruction of S : InsCode (IncAddr I,k) = InsCode J }
then consider J being Instruction of S such that
A1: a = AddressPart J and
A2: InsCode J = InsCode I ;
InsCode J = InsCode (IncAddr I,k) by A2, Def14;
hence a in { (AddressPart J) where J is Instruction of S : InsCode (IncAddr I,k) = InsCode J } by A1; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (AddressPart J) where J is Instruction of S : InsCode (IncAddr I,k) = InsCode J } or a in { (AddressPart J) where J is Instruction of S : InsCode I = InsCode J } )
assume a in { (AddressPart J) where J is Instruction of S : InsCode (IncAddr I,k) = InsCode J } ; :: thesis: a in { (AddressPart J) where J is Instruction of S : InsCode I = InsCode J }
then consider J being Instruction of S such that
A3: a = AddressPart J and
A4: InsCode J = InsCode (IncAddr I,k) ;
InsCode J = InsCode I by A4, Def14;
hence a in { (AddressPart J) where J is Instruction of S : InsCode I = InsCode J } by A3; :: thesis: verum

end;

hence AddressParts (InsCode I) = AddressParts (InsCode (IncAddr I,k)) ; :: thesis: verum