let I be set ; :: thesis: for M being V8() ManySortedSet of I holds not {} in rng M
let M be V8() 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 set st
( i in I & M . i = {} ) by A1, FUNCT_1:def 3;
hence contradiction by Def16; :: thesis: verum