A1: halt S in rng q by Def3;
rng q c= rng (p +* q) by FUNCT_4:18;
hence halt S in rng (p +* q) by A1; :: according to COMPOS_1:def 11 :: thesis: verum