reconsider f = {} as PartFunc of REAL,REAL by RELSET_1:12;
take f ; :: thesis: f is trivial
thus f is trivial ; :: thesis: verum