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

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 A2; :: thesis: verum

end;

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

A4: now

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

end;

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 ex m being Element of NAT st
( x = m & m < 0 + (len <*i*>) ) by A2;
then x = insloc 0 by A1, NAT_1:13;
hence x in {(insloc 0 )} by TARSKI:def 1; :: thesis: verum

end;

then dom (Load <*i*>) c= {(insloc 0 )} by TARSKI:def 3;
then ( dom ((insloc 0 ) .--> i) = {(insloc 0 )} & dom (Load <*i*>) = {(insloc 0 )} ) by A3, FUNCOP_1:19, XBOOLE_0:def 10;
hence Load <*i*> = (insloc 0 ) .--> i by A4, FUNCT_1:9; :: thesis: verum