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;
set IL = NAT ;
( 0 in {0 ,1} & 1 in {0 ,1} & 0 in ((union N) \/ (NAT \/ {NAT })) * ) by FINSEQ_1:66, TARSKI:def 2;
then ( [1,0 ] in [:NAT ,(((union N) \/ (NAT \/ {NAT })) * ):] & [0 ,0 ] in [:NAT ,(((union N) \/ (NAT \/ {NAT })) * ):] ) by ZFMISC_1:106;
then reconsider ins = {[1,0 ],[0 ,0 ]} as non empty Subset of [:NAT ,(((union N) \/ (NAT \/ {NAT })) * ):] by ZFMISC_1:38;
A1: dom ((NAT --> ins) +* (NAT .--> NAT )) = NAT \/ {NAT } by Lm3;
A2: rng (NAT --> ins) = {ins} by FUNCOP_1:14;
rng (NAT .--> NAT ) = {NAT } by FUNCOP_1:14;
then A3: rng ((NAT --> ins) +* (NAT .--> NAT )) c= {ins} \/ {NAT } by A2, FUNCT_4:18;
{ins} \/ {NAT } = {ins,NAT } by ENUMSET1:41;
then {ins} \/ {NAT } c= N \/ {ins,NAT } by XBOOLE_1:7;
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 A1, 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
.= (dom Ok) \/ {NAT } by CARD_3:18
.= dom Ok by A1, XBOOLE_1:7, XBOOLE_1:12 ; :: thesis:
let o be set ; :: thesis:
assume A5: o in dom Ok ; :: thesis:
then A6: ( o in NAT or o in {NAT } ) by XBOOLE_0:def 3;
A7: dom (NAT .--> (succ (s . NAT ))) = {NAT } by FUNCOP_1:19;

per cases by A6, TARSKI:def 1;

suppose o in NAT ; :: thesis:

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

end;

suppose A8: o = NAT ; :: thesis:

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

end;

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

end;

consider f being Function of (product Ok),(product Ok) such that
A15: for s being Element of product Ok holds f . s = H₁(s) from FUNCT_2:sch 8(A4);
set E = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product Ok)));
A16: dom (([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product Ok)))) = (dom ([1,0 ] .--> f)) \/ (dom ([0 ,0 ] .--> (id (product Ok)))) by FUNCT_4:def 1
.= {[1,0 ]} \/ (dom ([0 ,0 ] .--> (id (product Ok)))) by FUNCOP_1:19
.= {[1,0 ]} \/ {[0 ,0 ]} by FUNCOP_1:19
.= ins by ENUMSET1:41 ;
A17: rng (([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product Ok)))) c= (rng ([1,0 ] .--> f)) \/ (rng ([0 ,0 ] .--> (id (product Ok)))) by FUNCT_4:18;
A18: ( rng ([1,0 ] .--> f) c= {f} & rng ([0 ,0 ] .--> (id (product Ok))) c= {(id (product Ok))} ) by FUNCOP_1:19;
rng (([1,0 ] .--> f) +* ([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 ] .--> f) +* ([0 ,0 ] .--> (id (product Ok)))) ; :: thesis:
then ( e in rng ([1,0 ] .--> f) or e in rng ([0 ,0 ] .--> (id (product Ok))) ) by A17, XBOOLE_0:def 3;
then ( e = f or e = id (product Ok) ) by A18, TARSKI:def 1;
hence e in Funcs (product Ok),(product Ok) by FUNCT_2:12; :: thesis:

end;

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