set T = Trivial-AMI N;
reconsider la = NAT as Object of (Trivial-AMI N) by Def2;
consider l being Element of NAT ;
dom (NAT .--> NAT ) = {NAT } by FUNCOP_1:19;
then A1: NAT in dom (NAT .--> NAT ) by TARSKI:def 1;
ObjectKind la = ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )) . NAT by Def2
.= (NAT .--> NAT ) . NAT by A1, FUNCT_4:14
.= NAT by FUNCOP_1:87 ;
then reconsider a = l as Element of ObjectKind la ;
take la .--> a ; :: according to AMI_1:def 27 :: thesis: ( not la .--> a is empty & la .--> a is autonomic )
thus not la .--> a is empty ; :: thesis: la .--> a is autonomic
let s1, s2 be State of (Trivial-AMI N); :: according to AMI_1:def 25 :: thesis: ( la .--> a c= s1 & la .--> a c= s2 implies for i being Element of NAT holds (Computation s1,i) | (dom (la .--> a)) = (Computation s2,i) | (dom (la .--> a)) )
assume A2: ( la .--> a c= s1 & la .--> a c= s2 ) ; :: thesis: for i being Element of NAT holds (Computation s1,i) | (dom (la .--> a)) = (Computation s2,i) | (dom (la .--> a))
defpred S₁[ Element of NAT ] means (Computation s1,N) | (dom (la .--> a)) = (Computation s2,N) | (dom (la .--> a));

A3: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
set s3 = Computation s1,i;
set s4 = Computation s2,i;
(Computation s1,(i + 1)) | (dom (la .--> a)) = (Following (Computation s1,i)) | (dom (la .--> a)) by Th14
.= (Computation s1,i) | (dom (la .--> a)) by Th9
.= (Following (Computation s2,i)) | (dom (la .--> a)) by A4, Th9
.= (Computation s2,(i + 1)) | (dom (la .--> a)) by Th14 ;
hence S₁[i + 1] ; :: thesis: verum

end;

(Computation s1,0 ) | (dom (la .--> a)) = s1 | (dom (la .--> a)) by Th13
.= s2 | (dom (la .--> a)) by A2, GRFUNC_1:94
.= (Computation s2,0 ) | (dom (la .--> a)) by Th13 ;
then A5: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A5, A3); :: thesis: verum