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

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