set I = (insloc 0 ),(insloc 1) --> i,(halt SCM+FSA );
A1: dom ((insloc 0 ),(insloc 1) --> i,(halt SCM+FSA )) = {(insloc 0 ),(insloc 1)} by FUNCT_4:65;
reconsider I = (insloc 0 ),(insloc 1) --> i,(halt SCM+FSA ) as finite Function ;
A2: dom the Object-Kind of SCM+FSA = the carrier of SCM+FSA by FUNCT_2:def 1;

now

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

end;

then reconsider I = I as FinPartState of SCM+FSA by A1, A2, CARD_3:def 9;
( I is initial & I is NAT -defined )

proof

thus I is initial :: thesis: I is NAT -defined

proof

let m, n be Nat; :: according to SCMNORM:def 1 :: thesis: ( not n in dom I or n <= m or m in dom I )
assume that
A6: n in dom I and
A7: m < n ; :: thesis: m in dom I
( insloc n = insloc 0 or insloc n = insloc 1 ) by A1, A6, TARSKI:def 2;
then n = 0 + 1 by A7, NAT_1:2;
then m <= 0 by A7, NAT_1:13;
then m = 0 by NAT_1:3;
hence m in dom I by A1, TARSKI:def 2; :: thesis: verum

end;

thus dom I c= NAT by A1, ZFMISC_1:38; :: according to RELAT_1:def 18 :: thesis: verum

end;

hence (insloc 0 ),(insloc 1) --> i,(halt SCM+FSA ) is Program of SCM+FSA ; :: thesis: verum