consider D0 being non empty set such that
W: the Instructions of S c= [:NAT ,(NAT * ),(D0 * ):] by COMPOS_1:def 17;
set p = k + (JumpPart I);
set f = product" (JumpParts (InsCode I));
A8: JumpPart I in JumpParts (InsCode I) ;
A9: JumpParts (InsCode I) = product (product" (JumpParts (InsCode I))) by CARD_3:95;
A10: dom (k + (JumpPart I)) = dom (JumpPart I) by VALUED_1:def 2;
then B10: dom (k + (JumpPart I)) = DOM (JumpParts (InsCode I)) by A8, CARD_3:def 12
.= dom (product" (JumpParts (InsCode I))) by CARD_3:92 ;
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 A11: 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 A11;
A13: (product" (JumpParts (InsCode I))) . z = NAT by A11, A10, Def11;
reconsider il = (JumpPart I) . z as Element of NAT by ORDINAL1:def 13;
(k + (JumpPart I)) . z = k + il by A11, VALUED_1:def 2;
hence (k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z by A13; :: thesis: verum

end;

then k + (JumpPart I) in JumpParts (InsCode I) by A9, B10, CARD_3:18;
then consider II being Instruction of S such that
A14: k + (JumpPart I) = JumpPart II and
A15: InsCode I = InsCode II ;
X1: JumpPart I in JumpParts (InsCode I) ;
product (product" (JumpParts (InsCode I))) = JumpParts (InsCode I) by CARD_3:95;
then X2: JumpPart II in product (product" (JumpParts (InsCode I))) by A15;
I in the Instructions of S ;
then [(InsCode I),(JumpPart I),(AddressPart I)] = I by W, RECDEF_2:3;
then reconsider IT = [(InsCode I),(JumpPart II),(AddressPart I)] as Instruction of S by X1, X2, Dfs;
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 A14, RECDEF_2:def 2; :: thesis: verum