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

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

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

then
k + (JumpPart I) in JumpParts (InsCode I)
by A3, A5, CARD_3:9;
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;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

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