let i be Instruction of SCM+FSA ; :: thesis: Load <*i*> = 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 {0 } implies x in dom (Load <*i*>) )
assume x in {0 } ; :: thesis: x in dom (Load <*i*>)
then x = 0 by TARSKI:def 1;
hence x in dom (Load <*i*>) by A2; :: thesis: verum

end;

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

A4: now

let x be set ; :: thesis: ( x in {0 } implies (Load <*i*>) . x = (0 .--> i) . x )
assume A5: x in {0 } ; :: thesis: (Load <*i*>) . x = (0 .--> i) . x
then A6: x = 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
.= (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 {0 } )
assume x in dom (Load <*i*>) ; :: thesis: x in {0 }
then ex m being Element of NAT st
( x = m & m < 0 + (len <*i*>) ) by A2;
then x = 0 by A1, NAT_1:13;
hence x in {0 } by TARSKI:def 1; :: thesis: verum

end;

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