let n be object ; :: according to MEMSTR_0:def 3,FUNCT_1:def 9 :: thesis: ( not n in dom (the_Values_of (STC N)) or not (the_Values_of (STC N)) . n is empty )
set S = STC N;
set F = the_Values_of (STC N);
assume A1: n in dom (the_Values_of (STC N)) ; :: thesis: not (the_Values_of (STC N)) . n is empty
then A2: the Object-Kind of (STC N) . n in dom the ValuesF of (STC N) by FUNCT_1:11;
A3: the ValuesF of (STC N) = N --> NAT by Def7;
A4: the Object-Kind of (STC N) . n in N by A2;
(the_Values_of (STC N)) . n = the ValuesF of (STC N) . ( the Object-Kind of (STC N) . n) by A1, FUNCT_1:12
.= NAT by A4, A3, FUNCOP_1:7 ;
hence not (the_Values_of (STC N)) . n is empty ; :: thesis: verum