A1: dom p c= NAT by RELAT_1:def 18;
halt S in rng p by Def7;
then consider x being set such that
A2: x in dom p and
A3: p . x = halt S by FUNCT_1:def 3;
A4: x in dom (IncAddr (p,k)) by A2, Def40;
A5: Shift ((IncAddr (p,k)),k) = IncAddr ((Shift (p,k)),k) by Th121;
A6: dom (IncAddr (p,k)) c= NAT by RELAT_1:def 18;
reconsider m = x as Element of NAT by A1, A2;
(IncAddr (p,k)) . m = IncAddr ((p /. m),k) by A2, Def40
.= IncAddr ((halt S),k) by A3, A2, PARTFUN1:def 6
.= halt S by Th92 ;
then halt S in rng (IncAddr (p,k)) by A4, FUNCT_1:3;
hence halt S in rng (Reloc (p,k)) by A5, A6, VALUED_1:26; :: according to COMPOS_1:def 3 :: thesis: verum