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 )
A1: (Stop S) . 0 = halt S ;
A2: 0 in dom (Stop S) by Th2;
set pI = stop I;
card (stop I) = (card I) + 1 by Th39;
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 A1, A2, AFINSQ_1:def 3;
hence (stop I) . (card I) = halt S ; :: thesis: verum