set T = Trivial-AMI N;
set f = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT );
A1: product the Object-Kind of (Trivial-AMI N) = product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )) by Def2;
{[0 ,{} ]} = the Instructions of (Trivial-AMI N) by Def2;
then reconsider I = [0 ,{} ] as Instruction of (Trivial-AMI N) by TARSKI:def 1;
take I ; :: according to AMI_1:def 9 :: thesis: I is halting
let s be State of (Trivial-AMI N); :: according to AMI_1:def 8 :: thesis: Exec I,s = s
reconsider ss = s as Element of product the Object-Kind of (Trivial-AMI N) by PBOOLE:155;
(I .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ))))) . I = id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ))) by FUNCOP_1:87;
hence Exec I,s = (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) . ss by Def2
.= s by A1, FUNCT_1:35 ;
:: thesis: verum