set p = Load i;

now

let x be Element of 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 Th2;
then (Load i) . x = i by FUNCOP_1:87;
hence (Load i) . x <> halt SCMPDS by Def1; :: thesis: verum

end;

hence Load i is halt-free by Def3; :: thesis: verum