reconsider I = {[0 ,{} ]} as non empty set ;
set f = (IL --> I) +* (IL .--> IL);
A1: dom ((IL --> I) +* (IL .--> IL)) = (dom (IL --> I)) \/ (dom (IL .--> IL)) by FUNCT_4:def 1
.= IL \/ (dom (IL .--> IL)) by FUNCOP_1:19
.= succ IL by FUNCOP_1:19 ;
( rng (IL --> I) c= {I} & rng (IL .--> IL) c= {IL} ) by FUNCOP_1:19;
then (rng (IL --> I)) \/ (rng (IL .--> IL)) c= {I} \/ {IL} by XBOOLE_1:13;
then ( rng ((IL --> I) +* (IL .--> IL)) c= (rng (IL --> I)) \/ (rng (IL .--> IL)) & (rng (IL --> I)) \/ (rng (IL .--> IL)) c= {I,IL} ) by ENUMSET1:41, FUNCT_4:18;
then A2: rng ((IL --> I) +* (IL .--> IL)) c= {I,IL} by XBOOLE_1:1;
{I,IL} c= N \/ {I,IL} by XBOOLE_1:7;
then rng ((IL --> I) +* (IL .--> IL)) c= N \/ {I,IL} by A2, XBOOLE_1:1;
then reconsider f = (IL --> I) +* (IL .--> IL) as Function of (succ IL),(N \/ {I,IL}) by A1, FUNCT_2:def 1, RELSET_1:11;
reconsider y = IL as Element of succ IL 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 IL),y,I,f,E #); :: thesis: ( the carrier of S = succ IL & the Instruction-Counter of S = IL & the Instructions of S = {[0 ,{} ]} & the Object-Kind of S = (IL --> {[0 ,{} ]}) +* (IL .--> IL) & the Execution of S = [0 ,{} ] .--> (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)))) )
thus ( the carrier of S = succ IL & the Instruction-Counter of S = IL & the Instructions of S = {[0 ,{} ]} & the Object-Kind of S = (IL --> {[0 ,{} ]}) +* (IL .--> IL) & the Execution of S = [0 ,{} ] .--> (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)))) ) ; :: thesis: verum