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