IC = 0 by Def1;
hence Values (IC ) = (0 .--> NAT) . 0 by Lm1
.= NAT by FUNCOP_1:72 ;
:: according to MEMSTR_0:def 6 :: thesis: verum