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