reconsider I = {[0,{},{}]} as non empty set ;
reconsider i = [0,{},{}] as Element of I by TARSKI:def 1;
set f = (NAT --> I) +* (NAT .--> NAT);
A1: dom ((NAT --> I) +* (NAT .--> NAT)) =
(dom (NAT --> I)) \/ (dom (NAT .--> NAT))
by FUNCT_4:def 1
.=
NAT \/ (dom (NAT .--> NAT))
by FUNCOP_1:19
.=
succ NAT
by FUNCOP_1:19
;
( rng (NAT --> I) c= {I} & rng (NAT .--> NAT) c= {NAT} )
by FUNCOP_1:19;
then
(rng (NAT --> I)) \/ (rng (NAT .--> NAT)) c= {I} \/ {NAT}
by XBOOLE_1:13;
then
( rng ((NAT --> I) +* (NAT .--> NAT)) c= (rng (NAT --> I)) \/ (rng (NAT .--> NAT)) & (rng (NAT --> I)) \/ (rng (NAT .--> NAT)) c= {I,NAT} )
by ENUMSET1:41, FUNCT_4:18;
then A2:
rng ((NAT --> I) +* (NAT .--> NAT)) c= {I,NAT}
by XBOOLE_1:1;
{I,NAT} c= N \/ {I,NAT}
by XBOOLE_1:7;
then
rng ((NAT --> I) +* (NAT .--> NAT)) c= N \/ {I,NAT}
by A2, XBOOLE_1:1;
then reconsider f = (NAT --> I) +* (NAT .--> NAT) as Function of (succ NAT),(N \/ {I,NAT}) by A1, FUNCT_2:def 1, RELSET_1:11;
reconsider y = NAT as Element of succ NAT by ORDINAL1:10;
reconsider E = I --> (id (product f)) as Action of I,(product f) by FUNCOP_1:57, FUNCT_2:12;
take
AMI-Struct(# (succ NAT),y,I,i,f,E #)
; ( the carrier of AMI-Struct(# (succ NAT),y,I,i,f,E #) = succ NAT & the Instruction-Counter of AMI-Struct(# (succ NAT),y,I,i,f,E #) = NAT & the Instructions of AMI-Struct(# (succ NAT),y,I,i,f,E #) = {[0,{},{}]} & the haltF of AMI-Struct(# (succ NAT),y,I,i,f,E #) = [0,{},{}] & the Object-Kind of AMI-Struct(# (succ NAT),y,I,i,f,E #) = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of AMI-Struct(# (succ NAT),y,I,i,f,E #) = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) )
thus
( the carrier of AMI-Struct(# (succ NAT),y,I,i,f,E #) = succ NAT & the Instruction-Counter of AMI-Struct(# (succ NAT),y,I,i,f,E #) = NAT & the Instructions of AMI-Struct(# (succ NAT),y,I,i,f,E #) = {[0,{},{}]} & the haltF of AMI-Struct(# (succ NAT),y,I,i,f,E #) = [0,{},{}] & the Object-Kind of AMI-Struct(# (succ NAT),y,I,i,f,E #) = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of AMI-Struct(# (succ NAT),y,I,i,f,E #) = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) )
; verum