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
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
; ( InsCode IT = InsCode I & AddressPart IT = AddressPart I & JumpPart IT = k + (JumpPart I) )
thus
InsCode IT = InsCode I
; ( AddressPart IT = AddressPart I & JumpPart IT = k + (JumpPart I) )
thus
AddressPart IT = AddressPart I
; JumpPart IT = k + (JumpPart I)
thus
JumpPart IT = k + (JumpPart I)
by A9; verum