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;
A1: 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 A1, 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;
A2: dom ((NAT --> ins) +* (NAT .--> NAT)) = NAT \/ {NAT} by Lm3;
{ins} \/ {NAT} = {ins,NAT} by ENUMSET1:41;
then A3: {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 A3, XBOOLE_1:1;
then reconsider Ok = (NAT --> ins) +* (NAT .--> NAT) as Function of (NAT \/ {NAT}),(N \/ {ins,NAT}) by A2, FUNCT_2:def 1, RELSET_1:11;
deffunc H₁( Element of product Ok) -> set = $1 +* (NAT .--> (succ ($1 . NAT)));

A4: now

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

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 A2, XBOOLE_1:7, XBOOLE_1:12 ; :: thesis:
let o be set ; :: thesis:
A5: dom (NAT .--> (succ (s . NAT))) = {NAT} by FUNCOP_1:19;
assume A6: o in dom Ok ; :: thesis:
then A7: ( o in NAT or o in {NAT} ) by XBOOLE_0:def 3;

per cases by A7, 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 A5, FUNCT_4:12;
hence (s +* (NAT .--> (succ (s . NAT)))) . o in Ok . o by A6, CARD_3:18; :: thesis:

end;

suppose A8: o = NAT ; :: thesis:

A9: 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 A10: Ok . o = (NAT .--> NAT) . NAT by A8, FUNCT_4:14
.= NAT by A9, FUNCOP_1:13 ;
A11: o in {NAT} by A8, TARSKI:def 1;
then A12: (s +* (NAT .--> (succ (s . NAT)))) . o = (NAT .--> (succ (s . NAT))) . o by A5, FUNCT_4:14
.= succ (s . NAT) by A11, FUNCOP_1:13 ;
NAT in {NAT} by TARSKI:def 1;
then NAT in dom Ok by A2, XBOOLE_0:def 3;
then reconsider k = s . NAT as Element of NAT by A8, A10, CARD_3:18;
succ k in NAT ;
hence (s +* (NAT .--> (succ (s . NAT)))) . o in Ok . o by A10, A12; :: 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
A13: for s being Element of product Ok holds f . s = H₁(s) from FUNCT_2:sch 8(A4);
set E = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product Ok)));
A14: 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 ;
A15: ( rng ([1,0,0] .--> f) c= {f} & rng ([0,0,0] .--> (id (product Ok))) c= {(id (product Ok))} ) by FUNCOP_1:19;
A16: 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))

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 A16, XBOOLE_0:def 3;
then ( e = f or e = id (product Ok) ) by A15, 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 A14, 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 ZeroF 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 A13; :: 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: