let S be COM-Struct ; :: thesis: 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; :: thesis: for k being Nat holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
let k be Nat; :: thesis: 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 ; :: thesis: verum