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 (Macro i) = {0 ,1} by Th4;
A3: 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 A4: 2 in dom <*i,(halt SCM+FSA )*> by TARSKI:def 2;
A5: 1 in dom <*i,(halt SCM+FSA )*> by A3, TARSKI:def 2;

now

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

end;

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

A7: now

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

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

suppose A9: x = 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 A6, A8, SCMFSA_7:def 1
.= <*i,(halt SCM+FSA )*> . 1 by A5, PARTFUN1:def 8
.= (<*i*> ^ <*(halt SCM+FSA )*>) . 1
.= i by FINSEQ_1:58
.= (Macro i) . x by A9, SCMFSA6B:33 ;
:: thesis: verum

end;

suppose A10: x = 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 A6, A8, SCMFSA_7:def 1
.= <*i,(halt SCM+FSA )*> . 2 by A4, PARTFUN1:def 8
.= (<*i*> ^ <*(halt SCM+FSA )*>) . (1 + 1)
.= (<*i*> ^ <*(halt SCM+FSA )*>) . ((len <*i*>) + 1) by FINSEQ_1:57
.= halt SCM+FSA by FINSEQ_1:59
.= (Macro i) . x by A10, SCMFSA6B:33 ;
:: thesis: verum

end;

end;

end;

now

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

end;

then dom (Load <*i,(halt SCM+FSA )*>) c= {0 ,1} by TARSKI:def 3;
then dom (Load <*i,(halt SCM+FSA )*>) = {0 ,1} by A6, XBOOLE_0:def 10;
hence Macro i = Load <*i,(halt SCM+FSA )*> by A2, A7, FUNCT_1:9; :: thesis: verum