A: halt S in rng q by Def7;
ProgramPart (p +* q) = (ProgramPart p) +* (q | NAT) by FUNCT_4:75
.= (ProgramPart p) +* q by RELAT_1:209 ;
then rng q c= rng (ProgramPart (p +* q)) by FUNCT_4:19;
hence halt S in rng (ProgramPart (p +* q)) by A; :: according to COMPOS_1:def 7 :: thesis: verum