let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis: for p, q being NAT -defined the Instructions 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 Instructions 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))
thus Reloc ((p +* q),k) = IncAddr (((Shift (p,k)) +* (Shift (q,k))),k) by VALUED_1:23
.= (Reloc (p,k)) +* (Reloc (q,k)) by Th153 ; :: thesis: verum