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

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