consider f being non empty homogeneous PartFunc of ({{} } * ),{{} };
take f ; :: thesis: ( f is homogeneous & not f is empty )
thus ( f is homogeneous & not f is empty ) ; :: thesis: verum