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