set I = {[0,{},{}]};
reconsider i = [0,{},{}] as Element of {[0,{},{}]} by TARSKI:def 1;
set f = 0 .--> 0;
A1: dom (0 .--> 0) = dom (0 .--> 0)
.= {0} ;
A2: rng (0 .--> 0) c= {0} by FUNCOP_1:13;
0 in N by MEASURE6:def 2;
then {0} c= N by ZFMISC_1:31;
then rng (0 .--> 0) c= N by A2, XBOOLE_1:1;
then reconsider f = 0 .--> 0 as Function of {0},N by A1, RELSET_1:4;
reconsider y = 0 as Element of {0} by TARSKI:def 1;
set E = id (product ((N --> NAT) * f));
id (product ((N --> NAT) * f)) in Funcs ((product ((N --> NAT) * f)),(product ((N --> NAT) * f))) by FUNCT_2:9;
then reconsider F = {[0,{},{}]} --> (id (product ((N --> NAT) * f))) as Action of {[0,{},{}]},(product ((N --> NAT) * f)) by FUNCOP_1:45;
take AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),F #) ; :: thesis:
thus ( the carrier of AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),F #) = {0} & the ZeroF of AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),F #) = 0 & the InstructionsF of AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),F #) = {[0,{},{}]} & the Object-Kind of AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),F #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),F #) = N --> NAT & the Execution of AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),F #) = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) ; :: thesis: