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 4;
assume {} in rng M ; :: thesis: contradiction
then ex i being set st
( i in I & M . i = {} ) by A1, FUNCT_1:def 5;
hence contradiction by Def16; :: thesis: verum