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

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