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; COMPOS_1:def 11 verum