let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I being Element of the Instructions of S holds IncAddr I,0 = I
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for I being Element of the Instructions of S holds IncAddr I,0 = I
let I be Element of the Instructions of S; :: thesis: IncAddr I,0 = I
A1: InsCode (IncAddr I,0 ) = InsCode I by Def14;
XX: AddressPart (IncAddr I,0 ) = AddressPart I by Def14;
YY: JumpPart (IncAddr I,0 ) = 0 + (JumpPart I) by Def14;
then A2: dom (JumpPart I) = dom (JumpPart (IncAddr I,0 )) by VALUED_1:def 2;
for k being Nat st k in dom (JumpPart I) holds
(JumpPart (IncAddr I,0 )) . k = (JumpPart I) . k

proof

let k be Nat; :: thesis: ( k in dom (JumpPart I) implies (JumpPart (IncAddr I,0 )) . k = (JumpPart I) . k )
assume k in dom (JumpPart I) ; :: thesis: (JumpPart (IncAddr I,0 )) . k = (JumpPart I) . k
hence (JumpPart (IncAddr I,0 )) . k = 0 + ((JumpPart I) . k) by A2, YY, VALUED_1:def 2
.= (JumpPart I) . k ;
:: thesis: verum

end;

then JumpPart (IncAddr I,0 ) = JumpPart I by A2, FINSEQ_1:17;
hence IncAddr I,0 = I by A1, XX, COMPOS_1:7; :: thesis: verum