reconsider I = {[0,{},{}]} as non empty set ;
reconsider i = [0,{},{}] as Element of I by TARSKI:def 1;
set f = NAT .--> NAT;
A1: dom (NAT .--> NAT) = dom (NAT .--> NAT)
.= dom (NAT .--> NAT)
.= {NAT} by FUNCOP_1:13 ;
rng (NAT .--> NAT) c= {NAT} by FUNCOP_1:13;
then rng (NAT .--> NAT) c= {NAT} ;
then ( rng (NAT .--> NAT) c= rng (NAT .--> NAT) & rng (NAT .--> NAT) c= {NAT} ) ;
then A2: rng (NAT .--> NAT) c= {NAT} ;
{NAT} c= N \/ {NAT} by XBOOLE_1:7;
then rng (NAT .--> NAT) c= N \/ {NAT} by A2, XBOOLE_1:1;
then reconsider f = NAT .--> NAT as Function of {NAT},(N \/ {NAT}) by A1, RELSET_1:4;
reconsider y = NAT as Element of {NAT} by TARSKI:def 1;
reconsider E = I --> (id (product f)) as Action of I,(product f) by FUNCOP_1:45, FUNCT_2:9;
take S = AMI-Struct(# {NAT},y,I,i,f,E #); :: thesis: ( the carrier of S = {NAT} & the ZeroF of S = NAT & the Instructions of S = {[0,{},{}]} & the haltF of S = [0,{},{}] & the Object-Kind of S = NAT .--> NAT & the Execution of S = [0,{},{}] .--> (id (product (NAT .--> NAT))) )
thus ( the carrier of S = {NAT} & the ZeroF of S = NAT & the Instructions of S = {[0,{},{}]} & the haltF of S = [0,{},{}] & the Object-Kind of S = NAT .--> NAT & the Execution of S = [0,{},{}] .--> (id (product (NAT .--> NAT))) ) ; :: thesis: verum