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 S = COM-Struct(# (succ NAT ),y,I,i,f #); :: thesis: ( the carrier of S = succ NAT & the Instruction-Counter of S = NAT & the Instructions of S = {[0 ,{} ,{} ]} & the haltF of S = [0 ,{} ,{} ] & the Object-Kind of S = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) )
thus ( the carrier of S = succ NAT & the Instruction-Counter of S = NAT & the Instructions of S = {[0 ,{} ,{} ]} & the haltF of S = [0 ,{} ,{} ] & the Object-Kind of S = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) ) ; :: thesis: verum