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

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