thus Trivial-AMI E is IC-Ins-separated :: thesis: Trivial-AMI E is definite

proof

dom (NAT .--> NAT ) = {NAT } by FUNCOP_1:19;
then A1: NAT in dom (NAT .--> NAT ) by TARSKI:def 1;
IC (Trivial-AMI E) = NAT by Def2;
hence ObjectKind (IC (Trivial-AMI E)) = ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT )) . NAT by Def2
.= (NAT .--> NAT ) . NAT by A1, FUNCT_4:14
.= NAT by FUNCOP_1:87 ;
:: according to COMPOS_1:def 6 :: thesis: verum

end;

let l be Element of NAT ; :: according to COMPOS_1:def 8 :: thesis: the Object-Kind of (Trivial-AMI E) . l = the Instructions of (Trivial-AMI E)
A1: l in NAT ;

now

assume l in {NAT } ; :: thesis: contradiction
then l = NAT by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

then A2: not l in dom (NAT .--> NAT ) by FUNCOP_1:19;
thus the Object-Kind of (Trivial-AMI E) . l = ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT )) . l by Def2
.= (NAT --> {[0 ,{} ,{} ]}) . l by A2, FUNCT_4:12
.= {[0 ,{} ,{} ]} by FUNCOP_1:13
.= the Instructions of (Trivial-AMI E) by Def2 ; :: thesis: verum