set I = 0 ,1 --> i,(halt SCM+FSA );
A1: dom (0 ,1 --> i,(halt SCM+FSA )) = {0 ,1} by FUNCT_4:65;
X: dom (0 ,1 --> i,(halt SCM+FSA )) c= NAT by A1;
B1: dom (0 ,1 --> i,(halt SCM+FSA )) c= the carrier of SCM+FSA by X, XBOOLE_1:1;
reconsider I = 0 ,1 --> i,(halt SCM+FSA ) as finite Function ;

A2: now

rng I c= {i,(halt SCM+FSA )} by FUNCT_4:65;
then A3: rng I c= the Instructions of SCM+FSA by XBOOLE_1:1;
let x be set ; :: thesis: ( x in dom I implies I . x in the Object-Kind of SCM+FSA . x )
assume A4: x in dom I ; :: thesis: I . x in the Object-Kind of SCM+FSA . x
dom I c= NAT by A1;
then reconsider l = x as Element of NAT by A4;
A5: the Object-Kind of SCM+FSA . l = the Instructions of SCM+FSA by AMI_1:def 14;
I . x in rng I by A4, FUNCT_1:def 5;
hence I . x in the Object-Kind of SCM+FSA . x by A5, A3; :: thesis: verum

end;

reconsider I = I as FinPartState of SCM+FSA by B1, A2, FUNCT_1:def 20, RELAT_1:def 18;
A6: I is initial

proof

let m, n be Nat; :: according to SCMNORM:def 1 :: thesis: ( not n in proj1 I or n <= m or m in proj1 I )
assume that
A7: n in dom I and
A8: m < n ; :: thesis: m in proj1 I
( 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 I by A1, TARSKI:def 2; :: thesis: verum

end;

dom I c= NAT by A1;
hence 0 ,1 --> i,(halt SCM+FSA ) is Program of SCM+FSA by A6, RELAT_1:def 18; :: thesis: verum