let I be non empty set ; :: thesis: for B being V2() ManySortedSet of holds not union (rng B) is empty
let B be V2() ManySortedSet of ; :: thesis: not union (rng B) is empty
consider i being Element of I;
i in I ;
then i in dom B by PARTFUN1:def 4;
then ( B . i <> {} & B . i in rng B ) by FUNCT_1:def 5;
hence not union (rng B) is empty by ORDERS_1:91; :: thesis: verum