let S be COM-Struct ; :: thesis: for I being Program of S holds
( card I in dom (stop I) & (stop I) . (card I) = halt S )
let I be Program of S; :: thesis: ( card I in dom (stop I) & (stop I) . (card I) = halt S )
Lm1: (Stop S) . 0 = halt S by AFINSQ_1:34;
Lm2: 0 in dom (Stop S) by Th3;
set pI = stop I;
card (stop I) = (card I) + 1 by Th55;
then card I < card (stop I) by XREAL_1:29;
hence card I in dom (stop I) by AFINSQ_1:66; :: thesis: (stop I) . (card I) = halt S
(stop I) . (0 + (card I)) = halt S by Lm1, Lm2, AFINSQ_1:def 3;
hence (stop I) . (card I) = halt S ; :: thesis: verum