let IL be non empty set ; :: thesis: for E being set holds Trivial-AMI IL,E is definite
let E be set ; :: thesis: Trivial-AMI IL,E is definite
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