let i be Instruction of S; :: according to COMPOS_2:def 5 :: thesis: ( i in rng (Reloc (I,k)) implies rng (JumpPart i) c= dom (Reloc (I,k)) )
assume i in rng (Reloc (I,k)) ; :: thesis: rng (JumpPart i) c= dom (Reloc (I,k))
then consider n being object such that
A1: n in dom (Reloc (I,k)) and
A2: (Reloc (I,k)) . n = i by FUNCT_1:def 3;
dom (Reloc (I,k)) c= NAT by RELAT_1:def 18;
then reconsider n = n as Nat by A1;
A3: dom (Reloc (I,k)) = dom (Shift (I,k)) by COMPOS_1:32;
then consider j being Nat such that
A4: j in dom I and
A5: n = j + k by A1, VALUED_1:39;
I . j = I /. j by A4, PARTFUN1:def 6;
then reconsider i1 = I . j as Instruction of S ;
A6: IncAddr (i1,k) = i by A2, A4, A5, COMPOS_1:35;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (JumpPart i) or x in dom (Reloc (I,k)) )
assume A7: x in rng (JumpPart i) ; :: thesis: x in dom (Reloc (I,k))
then consider y being object such that
A8: y in dom (JumpPart i) and
A9: (JumpPart i) . y = x by FUNCT_1:def 3;
dom (JumpPart i) c= NAT by RELAT_1:def 18;
then reconsider y = y as Nat by A8;
A10: JumpPart i = (JumpPart i1) + k by A6, COMPOS_0:def 9;
then A11: dom (JumpPart i) = dom (JumpPart i1) by VALUED_1:def 2;
rng (JumpPart i) c= NAT by RELAT_1:def 19;
then reconsider m = x as Nat by A7;
reconsider n = (JumpPart i1) . y as Nat ;
A12: m = n + k by A9, A10, A8, VALUED_1:def 2;
A13: n in rng (JumpPart i1) by A8, A11, FUNCT_1:3;
i1 in rng I by A4, FUNCT_1:3;
then rng (JumpPart i1) c= dom I by Def5;
hence x in dom (Reloc (I,k)) by A3, A12, A13, VALUED_1:24; :: thesis: verum