let I be Program of ; :: thesis: for k being Nat holds UsedI*Loc I = UsedI*Loc (Reloc (I,k))
let k be Nat; :: thesis: UsedI*Loc I = UsedI*Loc (Reloc (I,k))
A1: Reloc (I,k) = IncAddr ((Shift (I,k)),k) by COMPOS_1:34;
UsedI*Loc (Reloc (I,k)) = UsedI*Loc (Reloc (I,k))
.= UsedI*Loc (Shift (I,k)) by Th40, A1
.= UsedI*Loc I by Th38 ;
hence UsedI*Loc I = UsedI*Loc (Reloc (I,k)) ; :: thesis: verum