set s = <%(halt S)%>;
A1: <%(halt S)%> = 0 .--> (halt S) by AFINSQ_1:def 2;
A2: 0 in NAT ;
NAT c= the carrier of S by AMI_1:def 3;
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 AMI_1:def 14;
then <%(halt S)%> in sproduct the Object-Kind of S by A1, 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 by RELAT_1:def 18; :: thesis: verum