let i be Instruction of S; :: according to COMPOS_2:def 5 :: thesis: ( i in rng (Reloc (I,k)) implies rng () c= dom (Reloc (I,k)) )
assume i in rng (Reloc (I,k)) ; :: thesis: rng () 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 ;
I . j = I /. j by ;
then reconsider i1 = I . j as Instruction of S ;
A6: IncAddr (i1,k) = i by ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng () or x in dom (Reloc (I,k)) )
assume A7: x in rng () ; :: thesis: x in dom (Reloc (I,k))
then consider y being object such that
A8: y in dom () and
A9: (JumpPart i) . y = x by FUNCT_1:def 3;
dom () c= NAT by RELAT_1:def 18;
then reconsider y = y as Nat by A8;
A10: JumpPart i = (JumpPart i1) + k by ;
then A11: dom () = dom (JumpPart i1) by VALUED_1:def 2;
rng () 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 ;
A13: n in rng (JumpPart i1) by ;
i1 in rng I by ;
then rng (JumpPart i1) c= dom I by Def5;
hence x in dom (Reloc (I,k)) by ; :: thesis: verum