theorem :: COMPOS_1:63

for S being COM-Struct
for loc being Nat
for I being initial preProgram of S st loc in dom I holds
(stop I) . loc = I . loc by AFINSQ_1:def 3;