let f be Function-yielding Function; :: thesis: ( 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; :: according to XBOOLE_0:def 10 :: thesis: ( 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:> :: thesis: rng <:f:> c= product (rngs f)

proof

set y = the Element of rng (doms f);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (doms f) or x in dom <:f:> )
assume A3: x in meet (doms f) ; :: thesis: 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; :: thesis: verum

end;

A10: dom (rngs f) = dom f by Def2;
thus rng <:f:> c= product (rngs f) :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( 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:> ; :: thesis: 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) :: according to XBOOLE_0:def 10 :: thesis: dom (rngs f) c= dom g

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom g or z in dom (rngs f) )
assume z in dom g ; :: thesis: 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; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum

end;

now :: thesis: for z being object st z in dom (rngs f) holds
g . z in (rngs f) . z

let z be object ; :: thesis: ( z in dom (rngs f) implies g . z in (rngs f) . z )
assume A25: z in dom (rngs f) ; :: thesis: g . z in (rngs f) . z
reconsider 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; :: thesis: verum

end;

hence y in product (rngs f) by A16, CARD_3:def 5; :: thesis: verum

end;