consider B being with_non-empty_elements set , f being Function of 0,B;
take product f ; :: thesis: ( product f is product-like & not product f is empty )
thus ( product f is product-like & not product f is empty ) ; :: thesis: verum