theorem :: MEMSTR_0:81

for N being with_zero set holds the_Values_of (Trivial-Mem N) = 0 .--> NAT by Lm1;