set T = Trivial-AMI N;
set f = NAT .--> NAT;
A1: product the Object-Kind of (Trivial-AMI N) = product (NAT .--> NAT) by Def1;
set I = the haltF of (Trivial-AMI N);
A2: the haltF of (Trivial-AMI N) = [0,{},{}] by Def1;
let s be State of (Trivial-AMI N); :: according to EXTPRO_1:def 3,EXTPRO_1:def 4 :: thesis: Exec ( the haltF of (Trivial-AMI N),s) = s
reconsider ss = s as Element of product the Object-Kind of (Trivial-AMI N) by CARD_3:107;
( the haltF of (Trivial-AMI N) .--> (id (product (NAT .--> NAT)))) . the haltF of (Trivial-AMI N) = id (product (NAT .--> NAT)) by FUNCOP_1:72;
hence Exec ( the haltF of (Trivial-AMI N),s) = (id (product (NAT .--> NAT))) . ss by A2, Def1
.= s by A1, FUNCT_1:18 ;
:: thesis: verum