let i be Instruction of ; :: 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) = {(insloc 0 ),(insloc 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 {(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, A5, A4; :: thesis: verum

end;

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

A7: now

let x be set ; :: thesis: ( x in {(insloc 0 ),(insloc 1)} implies (Load <*i,(halt SCM+FSA )*>) . b₁ = (Macro i) . b₁ )
assume A8: 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 A8, TARSKI:def 2;

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

end;

suppose A10: 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 A6, A8, SCMFSA_7:def 1
.= <*i,(halt SCM+FSA )*> . 2 by A4, 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 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 {(insloc 0 ),(insloc 1)} )
assume x in dom (Load <*i,(halt SCM+FSA )*>) ; :: thesis: x in {(insloc 0 ),(insloc 1)}
then ex m being Element of NAT st
( x = m -' 1 & m in dom <*i,(halt SCM+FSA )*> ) by A1;
then ( x = insloc ((0 + 1) -' 1) or x = insloc ((1 + 1) -' 1) ) by A3, 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 dom (Load <*i,(halt SCM+FSA )*>) c= {(insloc 0 ),(insloc 1)} by TARSKI:def 3;
then dom (Load <*i,(halt SCM+FSA )*>) = {(insloc 0 ),(insloc 1)} by A6, XBOOLE_0:def 10;
hence Macro i = Load <*i,(halt SCM+FSA )*> by A2, A7, FUNCT_1:9; :: thesis: verum