set P = I ^ J;
A1: not halt S in rng I by COMPOS_1:def 11;
A2: not halt S in rng J by COMPOS_1:def 11;
rng (I ^ J) = (rng I) \/ (rng J) by AFINSQ_1:26;
then not halt S in rng (I ^ J) by A1, A2, XBOOLE_0:def 3;
hence I ^ J is halt-free ; :: thesis: verum