set s = <%(halt S)%>;
A2: 0 in NAT ;
NAT c= the carrier of S by Def3;
then 0 in the carrier of S by A2;
then A3: 0 in dom the Object-Kind of S by FUNCT_2:def 1;
reconsider l = 0 as Element of NAT ;
halt S in the Instructions of S ;
then halt S in the Object-Kind of S . l by Def14;
then <%(halt S)%> in sproduct the Object-Kind of S by A3, CARD_3:76;
then reconsider s = <%(halt S)%> as FinPartState of S ;
dom s = 1 by AFINSQ_1:def 5;
then dom s c= NAT by CARD_1:87, ZFMISC_1:37;
hence <%(halt S)%> is Program of S ; :: thesis: verum