let I be non empty set ; :: thesis: for A being ManySortedSet of
for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
let A be ManySortedSet of ; :: thesis: for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
let B be ManySortedSubset of A; :: thesis: rng B c= union (rng (bool A))
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng B or a in union (rng (bool A)) )
assume a in rng B ; :: thesis: a in union (rng (bool A))
then consider i being set such that
A1: i in I and
A2: a = B . i by PBOOLE:150;
B c= A by PBOOLE:def 23;
then B in bool A by MBOOLEAN:19;
then B . i in (bool A) . i by A1, PBOOLE:def 4;
then A3: a in bool (A . i) by A1, A2, MBOOLEAN:def 1;
( i in dom (bool A) & bool (A . i) = (bool A) . i ) by A1, MBOOLEAN:def 1, PARTFUN1:def 4;
then bool (A . i) in rng (bool A) by FUNCT_1:def 5;
hence a in union (rng (bool A)) by A3, TARSKI:def 4; :: thesis: verum