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: 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, ZFMISC_1:38;
then reconsider l = x as Instruction-Location of SCM+FSA by A4, AMI_1:def 4;
A5: the Object-Kind of SCM+FSA . l = ObjectKind 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;

dom the Object-Kind of SCM+FSA = the carrier of SCM+FSA by FUNCT_2:def 1;
then reconsider I = I as FinPartState of by A1, A2, CARD_3:def 9;
A6: I is initial

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
A7: n in dom I and
A8: m < n ; :: thesis: m in dom I
( insloc n = insloc 0 or insloc n = insloc 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 dom I by A1, TARSKI:def 2; :: thesis: verum

end;

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