set O = {0};
reconsider IC1 = 0 as Element of {0} by TARSKI:def 1;
A1: 0 in NAT * by FINSEQ_1:49;
0 in ((union N) \/ {0}) * by FINSEQ_1:49;
then ( [1,0,0] in [:NAT,(NAT *),(((union N) \/ {0}) *):] & [0,0,0] in [:NAT,(NAT *),(((union N) \/ {0}) *):] ) by A1, MCART_1:69;
then reconsider ins = {[1,0,0],[0,0,0]} as non empty Subset of [:NAT,(NAT *),(((union N) \/ {0}) *):] by ZFMISC_1:32;
reconsider i = [0,0,0] as Element of ins by TARSKI:def 2;
A2: dom (0 .--> NAT) = {0} by FUNCOP_1:13;
A3: {NAT} c= N \/ {NAT} by XBOOLE_1:7;
rng (0 .--> NAT) c= N \/ {NAT} by A3, FUNCOP_1:8;
then reconsider Ok = 0 .--> NAT as Function of {0},(N \/ {NAT}) by A2, RELSET_1:4;
deffunc H₁( Element of product Ok) -> set = $1 +* (0 .--> (succ ($1 . 0)));

end;

end;

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:4;
set M = AMI-Struct(# {0},IC1,ins,i,Ok,E #);
take AMI-Struct(# {0},IC1,ins,i,Ok,E #) ; :: thesis:
thus the carrier of AMI-Struct(# {0},IC1,ins,i,Ok,E #) = {0} ; :: thesis:
thus the ZeroF of AMI-Struct(# {0},IC1,ins,i,Ok,E #) = 0 ; :: thesis:
thus the Instructions of AMI-Struct(# {0},IC1,ins,i,Ok,E #) = {[0,0,0],[1,0,0]} ; :: thesis:
thus the haltF of AMI-Struct(# {0},IC1,ins,i,Ok,E #) = [0,0,0] ; :: thesis:
thus the Object-Kind of AMI-Struct(# {0},IC1,ins,i,Ok,E #) = 0 .--> NAT ; :: thesis:
reconsider f = f as Function of (product the Object-Kind of AMI-Struct(# {0},IC1,ins,i,Ok,E #)),(product the Object-Kind of AMI-Struct(# {0},IC1,ins,i,Ok,E #)) ;
take f ; :: thesis:
thus for s being Element of product the Object-Kind of AMI-Struct(# {0},IC1,ins,i,Ok,E #) holds f . s = s +* (0 .--> (succ (s . 0))) by A13; :: thesis:
thus the Execution of AMI-Struct(# {0},IC1,ins,i,Ok,E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of AMI-Struct(# {0},IC1,ins,i,Ok,E #)))) ; :: thesis: