let f be Function; :: thesis: for F being Function-yielding Function st f = union (rng F) holds
dom f = union (rng (doms F))
let F be Function-yielding Function; :: thesis: ( f = union (rng F) implies dom f = union (rng (doms F)) )
assume A1: f = union (rng F) ; :: thesis: dom f = union (rng (doms F))
thus dom f c= union (rng (doms F)) :: according to XBOOLE_0:def 10 :: thesis: union (rng (doms F)) c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in union (rng (doms F)) )
assume x in dom f ; :: thesis: x in union (rng (doms F))
then [x,(f . x)] in union (rng F) by A1, FUNCT_1:def 2;
then consider g being set such that
A2: [x,(f . x)] in g and
A3: g in rng F by TARSKI:def 4;
consider u being object such that
A4: u in dom F and
A5: g = F . u by A3, FUNCT_1:def 3;
u in dom (doms F) by A4, A5, FUNCT_6:22;
then A6: (doms F) . u in rng (doms F) by FUNCT_1:def 3;
x in dom (F . u) by A2, A5, FUNCT_1:1;
then x in (doms F) . u by A4, FUNCT_6:22;
hence x in union (rng (doms F)) by A6, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng (doms F)) or x in dom f )
assume x in union (rng (doms F)) ; :: thesis: x in dom f
then consider A being set such that
A7: x in A and
A8: A in rng (doms F) by TARSKI:def 4;
consider u being object such that
A9: u in dom (doms F) and
A10: A = (doms F) . u by A8, FUNCT_1:def 3;
A11: u in dom F by A9, FUNCT_6:59;
then A12: F . u in rng F by FUNCT_1:def 3;
consider g being Function such that
A13: g = F . u ;
A = dom (F . u) by A10, A11, FUNCT_6:22;
then [x,(g . x)] in F . u by A7, A13, FUNCT_1:def 2;
then [x,(g . x)] in f by A1, A12, TARSKI:def 4;
hence x in dom f by FUNCT_1:1; :: thesis: verum