let I be Program of {INT,(INT *)}; :: thesis: for k being Element of NAT holds UsedInt*Loc I = UsedInt*Loc (ProgramPart (Relocated (I,k)))
let k be Element of NAT ; :: thesis: UsedInt*Loc I = UsedInt*Loc (ProgramPart (Relocated (I,k)))
UsedInt*Loc (ProgramPart (Relocated (I,k))) = UsedInt*Loc (Reloc ((ProgramPart I),k)) by COMPOS_1:116
.= UsedInt*Loc (Shift ((ProgramPart I),k)) by Th44
.= UsedInt*Loc (ProgramPart I) by Th42 ;
hence UsedInt*Loc I = UsedInt*Loc (ProgramPart (Relocated (I,k))) by RELAT_1:209; :: thesis: verum