let S be COM-Struct ; :: thesis: for i being Instruction of S holds rng (Macro i) = {i,(halt S)}
let i be Instruction of S; :: thesis: rng (Macro i) = {i,(halt S)}
thus rng (Macro i) = (rng (Load i)) \/ (rng (Stop S)) by AFINSQ_1:26
.= {i} \/ (rng (Stop S)) by AFINSQ_1:33
.= {i} \/ {(halt S)} by AFINSQ_1:33
.= {i,(halt S)} by ENUMSET1:1 ; :: thesis: verum