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