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