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