consider D0 being non empty set such that
A1: S c= [:NAT,(NAT *),(D0 *):] by Def1;
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:108
.= dom (product" (JumpParts (InsCode I))) by CARD_3:def 12 ;
for z being object st z in dom (k + (JumpPart I)) holds
(k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z

proof

let z be object ; :: 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 c= NAT by A6, A4, Lm2;
NAT c= (product" (JumpParts (InsCode I))) . z by A6, A4, Lm3;
then A8: (product" (JumpParts (InsCode I))) . z = NAT by A7;
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 A8; :: thesis: verum

end;

then k + (JumpPart I) in JumpParts (InsCode I) by A3, A5, CARD_3:9;
then consider II being Element of S such that
A9: k + (JumpPart I) = JumpPart II and
InsCode I = InsCode II ;
A10: JumpPart I in JumpParts (InsCode I) ;
[(InsCode I),(JumpPart I),(AddressPart I)] = I by A1, RECDEF_2:3;
then reconsider IT = [(InsCode I),(JumpPart II),(AddressPart I)] as Element of S by A10, Def6, A4, A9;
take IT ; :: thesis: ( InsCode IT = InsCode I & AddressPart IT = AddressPart I & JumpPart IT = k + (JumpPart I) )
thus InsCode IT = InsCode I ; :: thesis: ( AddressPart IT = AddressPart I & JumpPart IT = k + (JumpPart I) )
thus AddressPart IT = AddressPart I ; :: thesis: JumpPart IT = k + (JumpPart I)
thus JumpPart IT = k + (JumpPart I) by A9; :: thesis: verum