F: dom p c= NAT by RELAT_1:def 18;
halt S in rng p by Def7;
then consider x being set such that
W1: x in dom p and
W2: p . x = halt S by FUNCT_1:def 5;
F1: x in dom (IncAddr (p,k)) by W1, Def15;
F2: Shift ((IncAddr (p,k)),k) = IncAddr ((Shift (p,k)),k) by Th75;
F3: dom (IncAddr (p,k)) c= NAT by RELAT_1:def 18;
reconsider m = x as Element of NAT by F, W1;
(IncAddr (p,k)) . m = IncAddr ((p /. m),k) by W1, Def15
.= IncAddr ((halt S),k) by W2, W1, PARTFUN1:def 8
.= halt S by Th29 ;
then halt S in rng (IncAddr (p,k)) by F1, FUNCT_1:12;
hence halt S in rng (Reloc (p,k)) by F2, F3, VALUED_1:27; :: according to COMPOS_1:def 7 :: thesis: verum