set f = 0 .--> 0;
A1:
dom (0 .--> 0) = {0}
;
A2:
rng (0 .--> 0) c= {0}
by FUNCOP_1:13;
0 in N
by MEASURE6:def 2;
then
{0} c= N
by ZFMISC_1:31;
then
rng (0 .--> 0) c= N
by A2, XBOOLE_1:1;
then reconsider f = 0 .--> 0 as Function of {0},N by A1, RELSET_1:4;
reconsider y = 0 as Element of {0} by TARSKI:def 1;
take
Mem-Struct(# {0},y,f,(N --> NAT) #)
; ( the carrier of Mem-Struct(# {0},y,f,(N --> NAT) #) = {0} & the ZeroF of Mem-Struct(# {0},y,f,(N --> NAT) #) = 0 & the Object-Kind of Mem-Struct(# {0},y,f,(N --> NAT) #) = 0 .--> 0 & the ValuesF of Mem-Struct(# {0},y,f,(N --> NAT) #) = N --> NAT )
thus
( the carrier of Mem-Struct(# {0},y,f,(N --> NAT) #) = {0} & the ZeroF of Mem-Struct(# {0},y,f,(N --> NAT) #) = 0 & the Object-Kind of Mem-Struct(# {0},y,f,(N --> NAT) #) = 0 .--> 0 & the ValuesF of Mem-Struct(# {0},y,f,(N --> NAT) #) = N --> NAT )
; verum