let f be Function-yielding Function; ( dom <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) )
set f9 = (uncurry' f) | [:(meet (doms f)),(dom f):];
dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) c= [:(meet (doms f)),(dom f):]
by RELAT_1:58;
hence A1:
dom <:f:> c= meet (doms f)
by FUNCT_5:25; XBOOLE_0:def 10 ( meet (doms f) c= dom <:f:> & rng <:f:> c= product (rngs f) )
A2:
dom (doms f) = dom f
by Def1;
thus
meet (doms f) c= dom <:f:>
rng <:f:> c= product (rngs f)proof
set y = the
Element of
rng (doms f);
let x be
object ;
TARSKI:def 3 ( not x in meet (doms f) or x in dom <:f:> )
assume A3:
x in meet (doms f)
;
x in dom <:f:>
then A4:
rng (doms f) <> {}
by SETFAM_1:def 1;
then A5:
x in the
Element of
rng (doms f)
by A3, SETFAM_1:def 1;
consider z being
object such that A6:
z in dom (doms f)
and A7:
the
Element of
rng (doms f) = (doms f) . z
by A4, FUNCT_1:def 3;
reconsider g =
f . z as
Function ;
A8:
z in dom f
by A2, A6;
then
the
Element of
rng (doms f) = dom g
by A7, Th18;
then A9:
[x,z] in dom (uncurry' f)
by A8, A5, FUNCT_5:39;
[x,z] in [:(meet (doms f)),(dom f):]
by A3, A8, ZFMISC_1:87;
then
[x,z] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):]
by A9, XBOOLE_0:def 4;
then
[x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):])
by RELAT_1:61;
then
x in proj1 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))
by XTUPLE_0:def 12;
hence
x in dom <:f:>
by FUNCT_5:def 1;
verum
end;
A10:
dom (rngs f) = dom f
by Def2;
thus
rng <:f:> c= product (rngs f)
verumproof
let y be
object ;
TARSKI:def 3 ( not y in rng <:f:> or y in product (rngs f) )
A11:
dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) = (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):]
by RELAT_1:61;
A12:
uncurry' f = ~ (uncurry f)
by FUNCT_5:def 4;
assume
y in rng <:f:>
;
y in product (rngs f)
then consider x being
object such that A13:
x in dom <:f:>
and A14:
y = <:f:> . x
by FUNCT_1:def 3;
reconsider g =
y as
Function by A14;
A15:
dom g = proj2 ((dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) /\ [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):])
by A13, A14, FUNCT_5:31;
A16:
dom g = dom (rngs f)
proof
thus
dom g c= dom (rngs f)
XBOOLE_0:def 10 dom (rngs f) c= dom gproof
let z be
object ;
TARSKI:def 3 ( not z in dom g or z in dom (rngs f) )
assume
z in dom g
;
z in dom (rngs f)
then
[x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):])
by A13, A14, FUNCT_5:31;
then
[x,z] in dom (uncurry' f)
by A11, XBOOLE_0:def 4;
then
[z,x] in dom (uncurry f)
by A12, FUNCT_4:42;
then consider y1 being
object ,
h being
Function,
y2 being
object such that A17:
[z,x] = [y1,y2]
and A18:
y1 in dom f
and
h = f . y1
and
y2 in dom h
by FUNCT_5:def 2;
A19:
z = y1
by A17, XTUPLE_0:1;
thus
z in dom (rngs f)
by A10, A18, A19;
verum
end;
let z be
object ;
TARSKI:def 3 ( not z in dom (rngs f) or z in dom g )
A20:
x in {x}
by TARSKI:def 1;
assume A21:
z in dom (rngs f)
;
z in dom g
reconsider h =
f . z as
Function ;
A22:
z in dom f
by A10, A21;
then
dom h = (doms f) . z
by Th18;
then
dom h in rng (doms f)
by A2, A10, A21, FUNCT_1:def 3;
then
x in dom h
by A1, A13, SETFAM_1:def 1;
then
[z,x] in dom (uncurry f)
by A22, FUNCT_5:def 2;
then A23:
[x,z] in dom (uncurry' f)
by A12, FUNCT_4:42;
[x,z] in [:(meet (doms f)),(dom f):]
by A1, A13, A22, ZFMISC_1:87;
then A24:
[x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):])
by A11, A23, XBOOLE_0:def 4;
then
z in proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))
by XTUPLE_0:def 13;
then
[x,z] in [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):]
by A20, ZFMISC_1:87;
then
[x,z] in (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) /\ [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):]
by A24, XBOOLE_0:def 4;
hence
z in dom g
by A15, XTUPLE_0:def 13;
verum
end;
now for z being object st z in dom (rngs f) holds
g . z in (rngs f) . zlet z be
object ;
( z in dom (rngs f) implies g . z in (rngs f) . z )assume A25:
z in dom (rngs f)
;
g . z in (rngs f) . zreconsider h =
f . z as
Function ;
A26:
z in dom f
by A10, A25;
then
dom h = (doms f) . z
by Th18;
then
dom h in rng (doms f)
by A2, A10, A25, FUNCT_1:def 3;
then A27:
x in dom h
by A1, A13, SETFAM_1:def 1;
then A28:
h . x in rng h
by FUNCT_1:def 3;
(
g . z = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . (
x,
z) &
[x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) )
by A13, A14, A16, A25, FUNCT_5:31;
then
(uncurry' f) . (
x,
z)
= g . z
by FUNCT_1:47;
then
g . z = h . x
by A26, A27, FUNCT_5:39;
hence
g . z in (rngs f) . z
by A26, A28, Th18;
verum end;
hence
y in product (rngs f)
by A16, CARD_3:def 5;
verum
end;