let i be Instruction of SCM+FSA ; :: thesis: Load <*i*> = (insloc 0 ) .--> i
A1: dom (Load <*i*>) = { m where m is Element of NAT : m < len <*i*> } by Th1;
A2: len <*i*> = 1 by FINSEQ_1:56;
A3: dom ((insloc 0 ) .--> i) = {(insloc 0 )} by FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in dom (Load <*i*>) implies x in {(insloc 0 )} )
assume x in dom (Load <*i*>) ; :: thesis: x in {(insloc 0 )}
then consider m being Element of NAT such that
A4: x = m and
A5: m < 0 + (len <*i*>) by A1;
m <= 0 by A2, A5, NAT_1:13;
then x = insloc 0 by A4;
hence x in {(insloc 0 )} by TARSKI:def 1; :: thesis: verum

end;

then A6: dom (Load <*i*>) c= {(insloc 0 )} by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in {(insloc 0 )} implies x in dom (Load <*i*>) )
assume x in {(insloc 0 )} ; :: thesis: x in dom (Load <*i*>)
then x = insloc 0 by TARSKI:def 1;
hence x in dom (Load <*i*>) by A1, A2; :: thesis: verum

end;

then A7: {(insloc 0 )} c= dom (Load <*i*>) by TARSKI:def 3;
then A8: dom (Load <*i*>) = {(insloc 0 )} by A6, XBOOLE_0:def 10;

now

let x be set ; :: thesis: ( x in {(insloc 0 )} implies (Load <*i*>) . x = ((insloc 0 ) .--> i) . x )
assume A9: x in {(insloc 0 )} ; :: thesis: (Load <*i*>) . x = ((insloc 0 ) .--> i) . x
then A10: x = insloc 0 by TARSKI:def 1;
hence (Load <*i*>) . x = <*i*> /. (0 + 1) by A7, A9, SCMFSA_7:def 1
.= <*i*> . 1 by A2, FINSEQ_4:24
.= i by FINSEQ_1:57
.= ((insloc 0 ) .--> i) . x by A10, FUNCOP_1:87 ;
:: thesis: verum

end;

hence Load <*i*> = (insloc 0 ) .--> i by A3, A8, FUNCT_1:9; :: thesis: verum