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