let UN be Universe; :: thesis: for I being Element of UN
for x being UN -valued ManySortedSet of I holds disjoint-union x is Subset of [:(union (rng x)),I:]
let I be Element of UN; :: thesis: for x being UN -valued ManySortedSet of I holds disjoint-union x is Subset of [:(union (rng x)),I:]
let x be UN -valued ManySortedSet of I; :: thesis: disjoint-union x is Subset of [:(union (rng x)),I:]
union (rng (disjoin x)) c= [:(union (rng x)),I:]

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in union (rng (disjoin x)) or o in [:(union (rng x)),I:] )
assume o in union (rng (disjoin x)) ; :: thesis: o in [:(union (rng x)),I:]
then consider o9 being set such that
A1: o in o9 and
A2: o9 in rng (disjoin x) by TARSKI:def 4;
consider y being object such that
A3: y in dom (disjoin x) and
A4: o9 = (disjoin x) . y by A2, FUNCT_1:def 3;
A5: y in dom x by A3, CARD_3:def 3;
A6: y in I by A3, PARTFUN1:def 2;
A7: o in [:(x . y),{y}:] by A1, A4, A5, CARD_3:def 3;

now :: thesis: for o being object st o in [:(x . y),{y}:] holds
o in [:(union (rng x)),I:]

let o be object ; :: thesis: ( o in [:(x . y),{y}:] implies o in [:(union (rng x)),I:] )
assume o in [:(x . y),{y}:] ; :: thesis: o in [:(union (rng x)),I:]
then consider o1, o2 being object such that
A8: o1 in x . y and
A9: o2 in {y} and
A10: o = [o1,o2] by ZFMISC_1:def 2;

now :: thesis: ( o1 in union (rng x) & o2 in I )

x . y in rng x by A5, FUNCT_1:def 3;
hence o1 in union (rng x) by A8, TARSKI:def 4; :: thesis: o2 in I
thus o2 in I by A6, A9, TARSKI:def 1; :: thesis: verum

end;

hence o in [:(union (rng x)),I:] by A10, ZFMISC_1:def 2; :: thesis: verum

end;

hence o in [:(union (rng x)),I:] by A7; :: thesis: verum

end;

hence disjoint-union x is Subset of [:(union (rng x)),I:] ; :: thesis: verum