consider D0 being non empty set such that
A1: the Instructions of S c= [:NAT,(NAT *),(D0 *):] by Def17;
set p = k + (JumpPart I);
set f = product" (JumpParts (InsCode I));
A2: JumpPart I in JumpParts (InsCode I) ;
A3: JumpParts (InsCode I) = product (product" (JumpParts (InsCode I))) by CARD_3:78;
A4: dom (k + (JumpPart I)) = dom (JumpPart I) by VALUED_1:def 2;
then A5: dom (k + (JumpPart I)) = DOM (JumpParts (InsCode I)) by A2, CARD_3:def 11
.= dom (product" (JumpParts (InsCode I))) by CARD_3:75 ;
for z being set st z in dom (k + (JumpPart I)) holds
(k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z

proof

let z be set ; :: thesis: ( z in dom (k + (JumpPart I)) implies (k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z )
assume A6: z in dom (k + (JumpPart I)) ; :: thesis: (k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z
reconsider z = z as Element of NAT by A6;
A7: (product" (JumpParts (InsCode I))) . z = NAT by A6, A4, Def35;
reconsider il = (JumpPart I) . z as Element of NAT by ORDINAL1:def 12;
(k + (JumpPart I)) . z = k + il by A6, VALUED_1:def 2;
hence (k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z by A7; :: thesis: verum

end;

then k + (JumpPart I) in JumpParts (InsCode I) by A3, A5, CARD_3:9;
then consider II being Instruction of S such that
A8: k + (JumpPart I) = JumpPart II and
A9: InsCode I = InsCode II ;
A10: JumpPart I in JumpParts (InsCode I) ;
product (product" (JumpParts (InsCode I))) = JumpParts (InsCode I) by CARD_3:78;
then A11: JumpPart II in product (product" (JumpParts (InsCode I))) by A9;
I in the Instructions of S ;
then [(InsCode I),(JumpPart I),(AddressPart I)] = I by A1, RECDEF_2:3;
then reconsider IT = [(InsCode I),(JumpPart II),(AddressPart I)] as Instruction of S by A10, A11, Def36;
take IT ; :: thesis: ( InsCode IT = InsCode I & AddressPart IT = AddressPart I & JumpPart IT = k + (JumpPart I) )
thus InsCode IT = InsCode I by RECDEF_2:def 1; :: thesis: ( AddressPart IT = AddressPart I & JumpPart IT = k + (JumpPart I) )
thus AddressPart IT = AddressPart I by RECDEF_2:def 3; :: thesis: JumpPart IT = k + (JumpPart I)
thus JumpPart IT = k + (JumpPart I) by A8, RECDEF_2:def 2; :: thesis: verum