IC = NAT by Def1;
hence ObjectKind (IC ) = (NAT .--> NAT) . NAT by Def1
.= (NAT .--> NAT) . NAT
.= NAT by FUNCOP_1:72 ;
:: according to MEMSTR_0:def 3 :: thesis: verum