let S be COM-Struct ; :: thesis: for I being Program of S
for loc being Nat st loc in dom I holds
loc in dom (stop I)
let I be Program of S; :: thesis: for loc being Nat st loc in dom I holds
loc in dom (stop I)
let loc be Nat; :: thesis: ( loc in dom I implies loc in dom (stop I) )
dom I c= dom (I ^ (Stop S)) by AFINSQ_1:21;
hence ( loc in dom I implies loc in dom (stop I) ) ; :: thesis: verum