consider D0 being non empty set such that
A1: S c= [:NAT,(),(D0 *):] by Def1;
set p = k + ();
set f = product" (JumpParts ());
A2: JumpPart I in JumpParts () ;
A3: JumpParts () = product (product" (JumpParts ())) by CARD_3:78;
A4: dom (k + ()) = dom () by VALUED_1:def 2;
then A5: dom (k + ()) = DOM (JumpParts ()) by
.= dom (product" (JumpParts ())) by CARD_3:def 12 ;
for z being object st z in dom (k + ()) holds
(k + ()) . z in (product" (JumpParts ())) . z
proof
let z be object ; :: thesis: ( z in dom (k + ()) implies (k + ()) . z in (product" (JumpParts ())) . z )
assume A6: z in dom (k + ()) ; :: thesis: (k + ()) . z in (product" (JumpParts ())) . z
reconsider z = z as Element of NAT by A6;
A7: (product" (JumpParts ())) . z c= NAT by A6, A4, Lm2;
NAT c= (product" (JumpParts ())) . z by A6, A4, Lm3;
then A8: (product" (JumpParts ())) . z = NAT by A7;
reconsider il = () . z as Element of NAT by ORDINAL1:def 12;
(k + ()) . z = k + il by ;
hence (k + ()) . z in (product" (JumpParts ())) . z by A8; :: thesis: verum
end;
then k + () in JumpParts () by ;
then consider II being Element of S such that
A9: k + () = JumpPart II and
InsCode I = InsCode II ;
A10: JumpPart I in JumpParts () ;
[(),(),()] = I by ;
then reconsider IT = [(),(JumpPart II),()] as Element of S by A10, Def6, A4, A9;
take IT ; :: thesis: ( InsCode IT = InsCode I & AddressPart IT = AddressPart I & JumpPart IT = k + () )
thus InsCode IT = InsCode I ; :: thesis: ( AddressPart IT = AddressPart I & JumpPart IT = k + () )
thus AddressPart IT = AddressPart I ; :: thesis: JumpPart IT = k + ()
thus JumpPart IT = k + () by A9; :: thesis: verum