set s = <%(halt S)%>;
B: <%(halt S)%> = 0 .--> (halt S) by AFINSQ_1:def 2;
D: 0 in NAT ;
NAT c= the carrier of S by AMI_1:def 3;
then 0 in the carrier of S by D;
then C: 0 in dom the Object-Kind of S by FUNCT_2:def 1;
reconsider l = 0 as Instruction-Location of S by AMI_1:def 4;
halt S in the Instructions of S ;
then halt S in ObjectKind l by AMI_1:def 14;
then reconsider s = <%(halt S)%> as FinPartState of S by B, C, CARD_3:76;
A: dom s = 1 by AFINSQ_1:def 5;
0 in NAT ;
then dom s c= NAT by A, CARD_1:87, ZFMISC_1:37;
hence <%(halt S)%> is Program of S by RELAT_1:def 18; :: thesis: verum