theorem :: COMPOS_1:62

for S being COM-Struct
for I being Program of S
for loc being Nat st loc in dom I holds
loc in dom (stop I)