set I = 0 ,1 --> i,(halt SCM+FSA );
A1: dom (0 ,1 --> i,(halt SCM+FSA )) = {0 ,1} by FUNCT_4:65;
A6: 0 ,1 --> i,(halt SCM+FSA ) is initial

proof

let m, n be Nat; :: according to AFINSQ_1:def 13 :: thesis: ( not n in proj1 (0 ,1 --> i,(halt SCM+FSA )) or n <= m or m in proj1 (0 ,1 --> i,(halt SCM+FSA )) )
assume that
A7: n in dom (0 ,1 --> i,(halt SCM+FSA )) and
A8: m < n ; :: thesis: m in proj1 (0 ,1 --> i,(halt SCM+FSA ))
( n = 0 or n = 1 ) by A1, A7, TARSKI:def 2;
then n = 0 + 1 by A8, NAT_1:2;
then m <= 0 by A8, NAT_1:13;
then m = 0 by NAT_1:3;
hence m in proj1 (0 ,1 --> i,(halt SCM+FSA )) by A1, TARSKI:def 2; :: thesis: verum

end;

thus 0 ,1 --> i,(halt SCM+FSA ) is Program of SCM+FSA by A1, A6, RELAT_1:def 18; :: thesis: verum