let I be set ; :: thesis: for M being non-empty ManySortedSet of I holds not {} in rng M
let M be non-empty ManySortedSet of I; :: thesis: not {} in rng M
A1: dom M = I by PARTFUN1:def 2;
assume {} in rng M ; :: thesis: contradiction
then ex i being object st
( i in I & M . i = {} ) by A1, FUNCT_1:def 3;
hence contradiction by Def13; :: thesis: verum