reconsider I = {[0 ,{} ]} as non empty set ;
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 Function of I,(Funcs (product f),(product f)) by FUNCOP_1:57, FUNCT_2:12;
take S = AMI-Struct(# (succ NAT ),y,I,f,E #); ( the carrier of S = succ NAT & the Instruction-Counter of S = NAT & the Instructions of S = {[0 ,{} ]} & the Object-Kind of S = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of S = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) )
thus
( the carrier of S = succ NAT & the Instruction-Counter of S = NAT & the Instructions of S = {[0 ,{} ]} & the Object-Kind of S = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of S = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) )
; verum