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}
by FUNCOP_1:13
;
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;
reconsider E = {[0,{},{}]} --> (id (product ((N --> NAT) * f))) as Action of {[0,{},{}]},(product ((N --> NAT) * f)) by FUNCOP_1:45, FUNCT_2:9;
take S = AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),E #); ( the carrier of S = {0} & the ZeroF of S = 0 & the InstructionsF of S = {[0,{},{}]} & the Object-Kind of S = 0 .--> 0 & the ValuesF of S = N --> NAT & the Execution of S = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) )
thus
( the carrier of S = {0} & the ZeroF of S = 0 & the InstructionsF of S = {[0,{},{}]} & the Object-Kind of S = 0 .--> 0 & the ValuesF of S = N --> NAT & the Execution of S = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) )
; verum