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