let i be Instruction of SCM+FSA ; :: thesis: Macro i = Load <*i,(halt SCM+FSA )*>
A1: dom (Load <*i,(halt SCM+FSA )*>) = { (m -' 1) where m is Element of NAT : m in dom <*i,(halt SCM+FSA )*> } by SCMFSA_7:def 1;
A2: dom <*i,(halt SCM+FSA )*> = Seg (len <*i,(halt SCM+FSA )*>) by FINSEQ_1:def 3
.= {1,2} by FINSEQ_1:4, FINSEQ_1:61 ;
then A3: ( 1 in dom <*i,(halt SCM+FSA )*> & 2 in dom <*i,(halt SCM+FSA )*> ) by TARSKI:def 2;
A4: dom (Macro i) = {(insloc 0 ),(insloc 1)} by Th4;

now

let x be set ; :: thesis: ( x in dom (Load <*i,(halt SCM+FSA )*>) implies x in {(insloc 0 ),(insloc 1)} )
assume x in dom (Load <*i,(halt SCM+FSA )*>) ; :: thesis: x in {(insloc 0 ),(insloc 1)}
then consider m being Element of NAT such that
A5: x = m -' 1 and
A6: m in dom <*i,(halt SCM+FSA )*> by A1;
( x = insloc ((0 + 1) -' 1) or x = insloc ((1 + 1) -' 1) ) by A2, A5, A6, TARSKI:def 2;
then ( x = insloc 0 or x = insloc 1 ) by NAT_D:34;
hence x in {(insloc 0 ),(insloc 1)} by TARSKI:def 2; :: thesis: verum

end;

then A7: dom (Load <*i,(halt SCM+FSA )*>) c= {(insloc 0 ),(insloc 1)} by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in {(insloc 0 ),(insloc 1)} implies x in dom (Load <*i,(halt SCM+FSA )*>) )
assume x in {(insloc 0 ),(insloc 1)} ; :: thesis: x in dom (Load <*i,(halt SCM+FSA )*>)
then ( x = insloc 0 or x = insloc 1 ) by TARSKI:def 2;
then ( x = insloc ((0 + 1) -' 1) or x = insloc ((1 + 1) -' 1) ) by NAT_D:34;
hence x in dom (Load <*i,(halt SCM+FSA )*>) by A1, A3; :: thesis: verum

end;

then A8: {(insloc 0 ),(insloc 1)} c= dom (Load <*i,(halt SCM+FSA )*>) by TARSKI:def 3;
then A9: dom (Load <*i,(halt SCM+FSA )*>) = {(insloc 0 ),(insloc 1)} by A7, XBOOLE_0:def 10;

now

let x be set ; :: thesis: ( x in {(insloc 0 ),(insloc 1)} implies (Load <*i,(halt SCM+FSA )*>) . b₁ = (Macro i) . b₁ )
assume A10: x in {(insloc 0 ),(insloc 1)} ; :: thesis: (Load <*i,(halt SCM+FSA )*>) . b₁ = (Macro i) . b₁

per cases ( x = insloc 0 or x = insloc 1 ) by A10, TARSKI:def 2;

suppose A11: x = insloc 0 ; :: thesis: (Load <*i,(halt SCM+FSA )*>) . b₁ = (Macro i) . b₁

hence (Load <*i,(halt SCM+FSA )*>) . x = <*i,(halt SCM+FSA )*> /. (0 + 1) by A8, A10, SCMFSA_7:def 1
.= <*i,(halt SCM+FSA )*> . 1 by A3, PARTFUN1:def 8
.= (<*i*> ^ <*(halt SCM+FSA )*>) . 1 by FINSEQ_1:def 9
.= i by FINSEQ_1:58
.= (Macro i) . x by A11, SCMFSA6B:33 ;
:: thesis: verum

end;

suppose A12: x = insloc 1 ; :: thesis: (Load <*i,(halt SCM+FSA )*>) . b₁ = (Macro i) . b₁

hence (Load <*i,(halt SCM+FSA )*>) . x = <*i,(halt SCM+FSA )*> /. (1 + 1) by A8, A10, SCMFSA_7:def 1
.= <*i,(halt SCM+FSA )*> . 2 by A3, PARTFUN1:def 8
.= (<*i*> ^ <*(halt SCM+FSA )*>) . (1 + 1) by FINSEQ_1:def 9
.= (<*i*> ^ <*(halt SCM+FSA )*>) . ((len <*i*>) + 1) by FINSEQ_1:57
.= halt SCM+FSA by FINSEQ_1:59
.= (Macro i) . x by A12, SCMFSA6B:33 ;
:: thesis: verum

end;

end;

end;

hence Macro i = Load <*i,(halt SCM+FSA )*> by A4, A9, FUNCT_1:9; :: thesis: verum