let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for p, q being NAT -defined the Instructions of b₁ -valued finite Function
for k being Element of NAT holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for p, q being NAT -defined the Instructions of S -valued finite Function
for k being Element of 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 Element of NAT holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
let k be Element of 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:24
.= (Reloc (p,k)) +* (Reloc (q,k)) by Th153 ; :: thesis: verum