set p = Load i;

now

let x be Nat; :: thesis: ( x in dom (Load i) implies (Load i) . x <> halt SCMPDS )
assume x in dom (Load i) ; :: thesis: (Load i) . x <> halt SCMPDS
then x = 0 by COMPOS_1:50;
then (Load i) . x = i by FUNCOP_1:72;
hence (Load i) . x <> halt SCMPDS by COMPOS_1:def 24; :: thesis: verum

end;

hence Load i is halt-free by COMPOS_1:def 25; :: thesis: verum