let IL be non empty set ; :: thesis: for E being set holds Trivial-AMI IL,E is IC-Ins-separated
let E be set ; :: thesis: Trivial-AMI IL,E is IC-Ins-separated
A1: IC (Trivial-AMI IL,E) = IL by Def2;
dom (IL .--> IL) = {IL} by FUNCOP_1:19;
then A2: IL in dom (IL .--> IL) by TARSKI:def 1;
thus ObjectKind (IC (Trivial-AMI IL,E)) = ((IL --> {[0 ,{} ]}) +* (IL .--> IL)) . IL by A1, Def2
.= (IL .--> IL) . IL by A2, FUNCT_4:14
.= IL by FUNCOP_1:87 ; :: according to AMI_1:def 11 :: thesis: verum