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

proof

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

end;

let l be Instruction-Location of Trivial-AMI IL,E; :: according to AMI_1:def 14 :: thesis: ObjectKind l = the Instructions of (Trivial-AMI IL,E)
A1: l in IL by Def4;

now

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

end;

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