for f being Function st f = {} holds
f is ManySortedSet of {} by PARTFUN1:def 2, RELAT_1:38, RELAT_1:def 18;