let N be with_zero set ; :: thesis: the_Values_of (Trivial-Mem N) = 0 .--> NAT
set S = Trivial-Mem N;
set f = the_Values_of (Trivial-Mem N);
set g = 0 .--> NAT;
the Object-Kind of (Trivial-Mem N) = 0 .--> 0 by Def1;
then A1: the_Values_of (Trivial-Mem N) = (N --> NAT) * (0 .--> 0) by Def1;
A2: dom (N --> NAT) = N ;
A3: rng (0 .--> 0) = {0} by FUNCOP_1:88;
A4: 0 in N by MEASURE6:def 2;
then {0} c= N by ZFMISC_1:31;
then A5: dom (the_Values_of (Trivial-Mem N)) = dom (0 .--> 0) by A1, A2, A3, RELAT_1:27
.= {0} ;
hence dom (the_Values_of (Trivial-Mem N)) = dom (0 .--> NAT) ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (the_Values_of (Trivial-Mem N)) or (the_Values_of (Trivial-Mem N)) . b₁ = (0 .--> NAT) . b₁ )
let x be object ; :: thesis: ( not x in dom (the_Values_of (Trivial-Mem N)) or (the_Values_of (Trivial-Mem N)) . x = (0 .--> NAT) . x )
assume A6: x in dom (the_Values_of (Trivial-Mem N)) ; :: thesis: (the_Values_of (Trivial-Mem N)) . x = (0 .--> NAT) . x
then A7: x = 0 by A5, TARSKI:def 1;
thus (the_Values_of (Trivial-Mem N)) . x = (N --> NAT) . ((0 .--> 0) . x) by A1, A6, FUNCT_1:12
.= (N --> NAT) . 0 by A7, FUNCOP_1:72
.= NAT by A4, FUNCOP_1:7
.= (0 .--> NAT) . x by A7, FUNCOP_1:72 ; :: thesis: verum