let I be non empty set ; :: thesis: for B being V2() ManySortedSet of I holds not union (rng B) is empty
let B be V2() ManySortedSet of I; :: thesis: not union (rng B) is empty
set i = the Element of I;
the Element of I in I ;
then the Element of I in dom B by PARTFUN1:def 2;
then B . the Element of I in rng B by FUNCT_1:def 3;
hence not union (rng B) is empty by ORDERS_1:6; :: thesis: verum