set T = Trivial-AMI N;
set f = (N --> NAT) * (0 .--> 0);
A1: ( the Object-Kind of (Trivial-AMI N) = 0 .--> 0 & the ValuesF of (Trivial-AMI N) = N --> NAT ) by Def1;
set I = halt (Trivial-AMI N);
let s be State of (Trivial-AMI N); :: according to EXTPRO_1:def 3,EXTPRO_1:def 4 :: thesis: Exec ((halt (Trivial-AMI N)),s) = s
reconsider ss = s as Element of product (the_Values_of (Trivial-AMI N)) by CARD_3:107;
((halt (Trivial-AMI N)) .--> (id (product ((N --> NAT) * (0 .--> 0))))) . (halt (Trivial-AMI N)) = id (product ((N --> NAT) * (0 .--> 0))) by FUNCOP_1:72;
hence Exec ((halt (Trivial-AMI N)),s) = (id (product ((N --> NAT) * (0 .--> 0)))) . ss by Def1
.= s by A1 ;
:: thesis: verum