set p = Load i;

now :: thesis: for x being Nat st x in dom (Load i) holds
(Load i) . x <> halt SCMPDS

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 ;
hence (Load i) . x <> halt SCMPDS by COMPOS_0:def 12; :: thesis: verum

end;

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