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) #) ; :: thesis: ( 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 ) ; :: thesis: verum