let f be 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) = f " (SubFuncs (rng f)) by Def2;
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 set ; :: 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 set 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;
f . z in SubFuncs (rng f) by A2, A6, FUNCT_1:def 7;
then reconsider g = f . z as Function by Def1;
A8: z in dom f by A2, A6, FUNCT_1:def 7;
then the Element of rng (doms f) = dom g by A7, Th31;
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 FUNCT_5:2;
hence x in dom <:f:> by FUNCT_5:def 1; :: thesis: verum

end;

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

proof

let y be set ; :: 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 set such that
A13: x in dom <:f:> and
A14: y = <:f:> . x by FUNCT_1:def 3;
reconsider g = y as Function by A13, A14, FUNCT_5:30;
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 set ; :: 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 set , h being Function, y2 being set such that
A17: [z,x] = [y1,y2] and
A18: y1 in dom f and
A19: h = f . y1 and
y2 in dom h by FUNCT_5:def 2;
A20: z = y1 by A17, ZFMISC_1:27;
h in rng f by A18, A19, FUNCT_1:def 3;
then f . z in SubFuncs (rng f) by A19, A20, Def1;
hence z in dom (rngs f) by A10, A18, A20, FUNCT_1:def 7; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in dom (rngs f) or z in dom g )
A21: x in {x} by TARSKI:def 1;
assume A22: z in dom (rngs f) ; :: thesis: z in dom g
then f . z in SubFuncs (rng f) by A10, FUNCT_1:def 7;
then reconsider h = f . z as Function by Def1;
A23: z in dom f by A10, A22, FUNCT_1:def 7;
then dom h = (doms f) . z by Th31;
then dom h in rng (doms f) by A2, A10, A22, FUNCT_1:def 3;
then x in dom h by A1, A13, SETFAM_1:def 1;
then [z,x] in dom (uncurry f) by A23, FUNCT_5:def 2;
then A24: [x,z] in dom (uncurry' f) by A12, FUNCT_4:42;
[x,z] in [:(meet (doms f)),(dom f):] by A1, A13, A23, ZFMISC_1:87;
then A25: [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A11, A24, XBOOLE_0:def 4;
then z in proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) by FUNCT_5:2;
then [x,z] in [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):] by A21, 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 A25, XBOOLE_0:def 4;
hence z in dom g by A15, FUNCT_5:2; :: thesis: verum

end;

now

let z be set ; :: thesis: ( z in dom (rngs f) implies g . z in (rngs f) . z )
assume A26: z in dom (rngs f) ; :: thesis: g . z in (rngs f) . z
then f . z in SubFuncs (rng f) by A10, FUNCT_1:def 7;
then reconsider h = f . z as Function by Def1;
A27: z in dom f by A10, A26, FUNCT_1:def 7;
then dom h = (doms f) . z by Th31;
then dom h in rng (doms f) by A2, A10, A26, FUNCT_1:def 3;
then A28: x in dom h by A1, A13, SETFAM_1:def 1;
then A29: 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, A26, FUNCT_5:31;
then (uncurry' f) . (x,z) = g . z by FUNCT_1:47;
then g . z = h . x by A27, A28, FUNCT_5:39;
hence g . z in (rngs f) . z by A27, A29, Th31; :: thesis: verum

end;

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

end;