let I be non empty set ; :: thesis: for A being ManySortedSet of I
for B being ManySortedSubset of A holds rng B c= union (rng (bool A))
let A be ManySortedSet of I; :: 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 object ; :: 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 object such that
A1: i in I and
A2: a = B . i by PBOOLE:138;
( i in dom (bool A) & bool (A . i) = (bool A) . i ) by A1, MBOOLEAN:def 1, PARTFUN1:def 2;
then A3: bool (A . i) in rng (bool A) by FUNCT_1:def 3;
B c= A by PBOOLE:def 18;
then B in bool A by MBOOLEAN:18;
then B . i in (bool A) . i by A1;
then a in bool (A . i) by A1, A2, MBOOLEAN:def 1;
hence a in union (rng (bool A)) by A3, TARSKI:def 4; :: thesis: verum