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

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