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