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