take the empty PartFunc of REAL,REAL ; :: thesis: the empty PartFunc of REAL,REAL is empty
thus the empty PartFunc of REAL,REAL is empty ; :: thesis: verum