let Z be set ; :: thesis: for M being ManySortedSet of Z st ( for x being set st x in Z holds
M . x is ManySortedSet of x ) holds
for f being Function st f = Union M holds
dom f = union Z
let M be ManySortedSet of Z; :: thesis: ( ( for x being set st x in Z holds
M . x is ManySortedSet of x ) implies for f being Function st f = Union M holds
dom f = union Z )
assume A1: for x being set st x in Z holds
M . x is ManySortedSet of x ; :: thesis: for f being Function st f = Union M holds
dom f = union Z
let f be Function; :: thesis: ( f = Union M implies dom f = union Z )
assume f = Union M ; :: thesis: dom f = union Z
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: ( x in dom f iff ex Y being set st
( x in Y & Y in Z ) )
thus ( x in dom f implies ex Y being set st
( x in Y & Y in Z ) ) :: thesis: ( ex Y being set st
( x in Y & Y in Z ) implies x in dom f )

proof

assume x in dom f ; :: thesis: ex Y being set st
( x in Y & Y in Z )
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: ( x in dom g & dom g in Z )
thus x in dom g by A3, FUNCT_1:1; :: thesis: dom g in Z
thus dom g in Z by A7, PARTFUN1:def 2; :: thesis: verum

end;

given Y being set such that A8: x in Y and
A9: Y in Z ; :: thesis: x in dom f
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: verum

end;

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