set a = the Function of (NAT \ {0}),INT;
take IT = Language-like(# NAT,0,0, the Function of (NAT \ {0}),INT #); :: thesis: ( IT is strict & not IT is empty )
thus ( IT is strict & not IT is empty ) ; :: thesis: verum