let S be COM-Struct ; for p, q being NAT -defined the InstructionsF of S -valued finite Function
for k being Nat holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
let p, q be NAT -defined the InstructionsF of S -valued finite Function; for k being Nat holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
let k be Nat; Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
A1:
Reloc ((p +* q),k) = IncAddr ((Shift ((p +* q),k)),k)
by Th22;
A2:
Reloc (p,k) = IncAddr ((Shift (p,k)),k)
by Th22;
A3:
Reloc (q,k) = IncAddr ((Shift (q,k)),k)
by Th22;
thus Reloc ((p +* q),k) =
IncAddr (((Shift (p,k)) +* (Shift (q,k))),k)
by A1, VALUED_1:23
.=
(Reloc (p,k)) +* (Reloc (q,k))
by A2, A3, Th25
; verum