let n be object ; :: according to FUNCT_1:def 9,MEMSTR_0:def 3 :: thesis: ( not n in proj1 (the_Values_of (Trivial-AMI N)) or not (the_Values_of (Trivial-AMI N)) . n is empty )

set S = Trivial-AMI N;

set F = the_Values_of (Trivial-AMI N);

assume A1: n in dom (the_Values_of (Trivial-AMI N)) ; :: thesis: not (the_Values_of (Trivial-AMI N)) . n is empty

then A2: the Object-Kind of (Trivial-AMI N) . n in dom the ValuesF of (Trivial-AMI N) by FUNCT_1:11;

A3: the ValuesF of (Trivial-AMI N) = N --> NAT by Def1;

then A4: the Object-Kind of (Trivial-AMI N) . n in N by A2;

(the_Values_of (Trivial-AMI N)) . n = the ValuesF of (Trivial-AMI N) . ( the Object-Kind of (Trivial-AMI N) . n) by A1, FUNCT_1:12

.= NAT by A4, A3, FUNCOP_1:7 ;

hence not (the_Values_of (Trivial-AMI N)) . n is empty ; :: thesis: verum

set S = Trivial-AMI N;

set F = the_Values_of (Trivial-AMI N);

assume A1: n in dom (the_Values_of (Trivial-AMI N)) ; :: thesis: not (the_Values_of (Trivial-AMI N)) . n is empty

then A2: the Object-Kind of (Trivial-AMI N) . n in dom the ValuesF of (Trivial-AMI N) by FUNCT_1:11;

A3: the ValuesF of (Trivial-AMI N) = N --> NAT by Def1;

then A4: the Object-Kind of (Trivial-AMI N) . n in N by A2;

(the_Values_of (Trivial-AMI N)) . n = the ValuesF of (Trivial-AMI N) . ( the Object-Kind of (Trivial-AMI N) . n) by A1, FUNCT_1:12

.= NAT by A4, A3, FUNCOP_1:7 ;

hence not (the_Values_of (Trivial-AMI N)) . n is empty ; :: thesis: verum