A1: dom p c= NAT by RELAT_1:def 18;
halt S in rng p by Def3;
then consider x being object 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, Def9;
A5: 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, Def9
.= IncAddr ((halt S),k) by A3, A2, PARTFUN1:def 6
.= halt S by COMPOS_0:4 ;
then halt S in rng (IncAddr (p,k)) by A4, FUNCT_1:3;
hence halt S in rng (Reloc (p,k)) by A5, VALUED_1:26; :: according to COMPOS_1:def 11 :: thesis: verum