set O = NAT \/ {NAT };
NAT in {NAT } by TARSKI:def 1;
then reconsider IC1 = NAT as Element of NAT \/ {NAT } by XBOOLE_0:def 3;
X: 0 in NAT * by FINSEQ_1:66;
0 in ((union N) \/ (NAT \/ {NAT })) * by FINSEQ_1:66;
then ( [1,0 ,0 ] in [:NAT ,(NAT * ),(((union N) \/ (NAT \/ {NAT })) * ):] & [0 ,0 ,0 ] in [:NAT ,(NAT * ),(((union N) \/ (NAT \/ {NAT })) * ):] ) by X, MCART_1:73;
then reconsider ins = {[1,0 ,0 ],[0 ,0 ,0 ]} as non empty Subset of [:NAT ,(NAT * ),(((union N) \/ (NAT \/ {NAT })) * ):] by ZFMISC_1:38;
reconsider i = [0 ,0 ,0 ] as Element of ins by TARSKI:def 2;
A1: dom ((NAT --> ins) +* (NAT .--> NAT )) = NAT \/ {NAT } by Lm3;
{ins} \/ {NAT } = {ins,NAT } by ENUMSET1:41;
then A2: {ins} \/ {NAT } c= N \/ {ins,NAT } by XBOOLE_1:7;
( rng (NAT --> ins) = {ins} & rng (NAT .--> NAT ) = {NAT } ) by FUNCOP_1:14;
then rng ((NAT --> ins) +* (NAT .--> NAT )) c= {ins} \/ {NAT } by FUNCT_4:18;
then rng ((NAT --> ins) +* (NAT .--> NAT )) c= N \/ {ins,NAT } by A2, XBOOLE_1:1;
then reconsider Ok = (NAT --> ins) +* (NAT .--> NAT ) as Function of (NAT \/ {NAT }),(N \/ {ins,NAT }) by A1, FUNCT_2:def 1, RELSET_1:11;
deffunc H₁( Element of product Ok) -> set = $1 +* (NAT .--> (succ ($1 . NAT )));

A3: now

let s be Element of product Ok; :: thesis:

now

thus dom (s +* (NAT .--> (succ (s . NAT )))) = (dom s) \/ (dom (NAT .--> (succ (s . NAT )))) by FUNCT_4:def 1
.= (dom s) \/ {NAT } by FUNCOP_1:19
.= (NAT \/ {NAT }) \/ {NAT } by PARTFUN1:def 4
.= dom Ok by A1, XBOOLE_1:7, XBOOLE_1:12 ; :: thesis:
let o be set ; :: thesis:
A4: dom (NAT .--> (succ (s . NAT ))) = {NAT } by FUNCOP_1:19;
assume A5: o in dom Ok ; :: thesis:
then A6: ( o in NAT or o in {NAT } ) by XBOOLE_0:def 3;

per cases by A6, TARSKI:def 1;

suppose o in NAT ; :: thesis:

then not o in {NAT } by TARSKI:def 1;
then (s +* (NAT .--> (succ (s . NAT )))) . o = s . o by A4, FUNCT_4:12;
hence (s +* (NAT .--> (succ (s . NAT )))) . o in Ok . o by A5, CARD_3:18; :: thesis:

end;

suppose A7: o = NAT ; :: thesis:

A8: NAT in {NAT } by TARSKI:def 1;
dom (NAT .--> NAT ) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> NAT ) by TARSKI:def 1;
then A9: Ok . o = (NAT .--> NAT ) . NAT by A7, FUNCT_4:14
.= NAT by A8, FUNCOP_1:13 ;
A10: o in {NAT } by A7, TARSKI:def 1;
then A11: (s +* (NAT .--> (succ (s . NAT )))) . o = (NAT .--> (succ (s . NAT ))) . o by A4, FUNCT_4:14
.= succ (s . NAT ) by A10, FUNCOP_1:13 ;
NAT in {NAT } by TARSKI:def 1;
then NAT in dom Ok by A1, XBOOLE_0:def 3;
then reconsider k = s . NAT as Element of NAT by A7, A9, CARD_3:18;
succ k in NAT ;
hence (s +* (NAT .--> (succ (s . NAT )))) . o in Ok . o by A9, A11; :: thesis:

end;

end;

end;

hence H₁(s) in product Ok by CARD_3:18; :: thesis:

end;

consider f being Function of (product Ok),(product Ok) such that
A12: for s being Element of product Ok holds f . s = H₁(s) from FUNCT_2:sch 8(A3);
set E = ([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product Ok)));
A13: dom (([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product Ok)))) = (dom ([1,0 ,0 ] .--> f)) \/ (dom ([0 ,0 ,0 ] .--> (id (product Ok)))) by FUNCT_4:def 1
.= {[1,0 ,0 ]} \/ (dom ([0 ,0 ,0 ] .--> (id (product Ok)))) by FUNCOP_1:19
.= {[1,0 ,0 ]} \/ {[0 ,0 ,0 ]} by FUNCOP_1:19
.= ins by ENUMSET1:41 ;
A14: ( rng ([1,0 ,0 ] .--> f) c= {f} & rng ([0 ,0 ,0 ] .--> (id (product Ok))) c= {(id (product Ok))} ) by FUNCOP_1:19;
A15: rng (([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product Ok)))) c= (rng ([1,0 ,0 ] .--> f)) \/ (rng ([0 ,0 ,0 ] .--> (id (product Ok)))) by FUNCT_4:18;
rng (([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product Ok)))) c= Funcs (product Ok),(product Ok)

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in rng (([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product Ok)))) ; :: thesis:
then ( e in rng ([1,0 ,0 ] .--> f) or e in rng ([0 ,0 ,0 ] .--> (id (product Ok))) ) by A15, XBOOLE_0:def 3;
then ( e = f or e = id (product Ok) ) by A14, TARSKI:def 1;
hence e in Funcs (product Ok),(product Ok) by FUNCT_2:12; :: thesis:

end;

then reconsider E = ([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product Ok))) as Function of ins,(Funcs (product Ok),(product Ok)) by A13, FUNCT_2:def 1, RELSET_1:11;
set M = AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #);
take AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #) ; :: thesis:
thus the carrier of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #) = NAT \/ {NAT } ; :: thesis:
thus the Instruction-Counter of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #) = NAT ; :: thesis:
thus the Instructions of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #) = {[0 ,0 ,0 ],[1,0 ,0 ]} ; :: thesis:
thus the haltF of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #) = [0 ,0 ,0 ] ; :: thesis:
thus the Object-Kind of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #) = (NAT --> {[1,0 ,0 ],[0 ,0 ,0 ]}) +* (NAT .--> NAT ) ; :: thesis:
reconsider f = f as Function of (product the Object-Kind of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #)),(product the Object-Kind of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #)) ;
take f ; :: thesis:
thus for s being Element of product the Object-Kind of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #) holds f . s = s +* (NAT .--> (succ (s . NAT ))) by A12; :: thesis:
thus the Execution of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #) = ([1,0 ,0 ] .--> f) +* ([0 ,0 ,0 ] .--> (id (product the Object-Kind of AMI-Struct(# (NAT \/ {NAT }),IC1,ins,i,Ok,E #)))) ; :: thesis: