let Z be set ; :: thesis:
let M be ManySortedSet of Z; :: thesis:
assume A1: for x being set st x in Z holds
M . x is ManySortedSet of x ; :: thesis:
let f be Function; :: thesis:
assume f = Union M ; :: thesis:
then A2: f = union (rng M) by CARD_3:def 4;
for x being object holds
( x in dom f iff ex Y being set st
( x in Y & Y in Z ) )

proof

let x be object ; :: thesis:
thus ( x in dom f implies ex Y being set st
( x in Y & Y in Z ) ) :: thesis:

proof

assume x in dom f ; :: thesis:
then [x,(f . x)] in f by FUNCT_1:def 2;
then consider g being set such that
A3: [x,(f . x)] in g and
A4: g in rng M by A2, TARSKI:def 4;
consider a being object such that
A5: a in dom M and
A6: g = M . a by A4, FUNCT_1:def 3;
reconsider a = a as set by TARSKI:1;
A7: a in Z by A5, PARTFUN1:def 2;
then reconsider g = g as ManySortedSet of a by A1, A6;
take dom g ; :: thesis:
thus x in dom g by A3, FUNCT_1:1; :: thesis:
thus dom g in Z by A7, PARTFUN1:def 2; :: thesis:

end;

given Y being set such that A8: x in Y and
A9: Y in Z ; :: thesis:
reconsider g = M . Y as ManySortedSet of Y by A1, A9;
Y = dom g by PARTFUN1:def 2;
then A10: [x,(g . x)] in g by A8, FUNCT_1:1;
Z = dom M by PARTFUN1:def 2;
then g in rng M by A9, FUNCT_1:def 3;
then [x,(g . x)] in f by A2, A10, TARSKI:def 4;
hence x in dom f by FUNCT_1:1; :: thesis:

end;

hence dom f = union Z by TARSKI:def 4; :: thesis: