set S = Trivial-AMI E;
A1: ( the Object-Kind of (Trivial-AMI E) = 0 .--> 0 & the ValuesF of (Trivial-AMI E) = E --> NAT ) by Def1;
A2: 0 in E by MEASURE6:def 2;
A3: 0 in dom (0 .--> 0) by FUNCOP_1:73;
thus Values (IC ) = (the_Values_of (Trivial-AMI E)) . 0 by Def1
.= ((E --> NAT) * (0 .--> 0)) . 0 by A1
.= (E --> NAT) . ((0 .--> 0) . 0) by A3, FUNCT_1:13
.= (E --> NAT) . 0 by FUNCOP_1:72
.= NAT by A2, FUNCOP_1:7 ; :: according to MEMSTR_0:def 6 :: thesis: verum