let f be Function; for F being Function-yielding Function st f = union (rng F) holds
dom f = union (rng (doms F))
let F be Function-yielding Function; ( f = union (rng F) implies dom f = union (rng (doms F)) )
assume A1:
f = union (rng F)
; dom f = union (rng (doms F))
thus
dom f c= union (rng (doms F))
XBOOLE_0:def 10 union (rng (doms F)) c= dom fproof
let x be
object ;
TARSKI:def 3 ( not x in dom f or x in union (rng (doms F)) )
assume
x in dom f
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in union (rng (doms F)) or x in dom f )
assume
x in union (rng (doms F))
; 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; verum