ProgramPart p <> {} by Def29;
then Reloc ((ProgramPart p),k) <> {} ;
then A: (Reloc ((ProgramPart p),k)) | NAT <> {} by RELAT_1:209;
(Relocated (p,k)) | NAT = (ProgramPart (IncrIC ((NPP p),k))) +* ((Reloc ((ProgramPart p),k)) | NAT) by FUNCT_4:75
.= {} +* ((Reloc ((ProgramPart p),k)) | NAT) by Th152
.= (Reloc ((ProgramPart p),k)) | NAT by FUNCT_4:21 ;
hence (Relocated (p,k)) | NAT <> {} by A; :: according to COMPOS_1:def 29 :: thesis: verum