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:87;
hence A1: dom <:f:> c= meet (doms f) by FUNCT_5:32; :: 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

consider y being 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 y by A3, SETFAM_1:def 1;
consider z being set such that
A6: z in dom (doms f) and
A7: y = (doms f) . z by A4, FUNCT_1:def 5;
f . z in SubFuncs (rng f) by A2, A6, FUNCT_1:def 13;
then reconsider g = f . z as Function by Def1;
A8: z in dom f by A2, A6, FUNCT_1:def 13;
then y = dom g by A7, Th31;
then A9: [x,z] in dom (uncurry' f) by A8, A5, FUNCT_5:46;
[x,z] in [:(meet (doms f)),(dom f):] by A3, A8, ZFMISC_1:106;
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:90;
then x in proj1 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) by FUNCT_5:4;
hence x in dom <:f:> by FUNCT_5:def 3; :: 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:90;
A12: uncurry' f = ~ (uncurry f) by FUNCT_5:def 6;
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 5;
reconsider g = y as Function by A13, A14, FUNCT_5:37;
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:38;
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:38;
then [x,z] in dom (uncurry' f) by A11, XBOOLE_0:def 4;
then [z,x] in dom (uncurry f) by A12, FUNCT_4:43;
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 4;
A20: z = y1 by A17, ZFMISC_1:33;
h in rng f by A18, A19, FUNCT_1:def 5;
then f . z in SubFuncs (rng f) by A19, A20, Def1;
hence z in dom (rngs f) by A10, A18, A20, FUNCT_1:def 13; :: 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 13;
then reconsider h = f . z as Function by Def1;
A23: z in dom f by A10, A22, FUNCT_1:def 13;
then dom h = (doms f) . z by Th31;
then dom h in rng (doms f) by A2, A10, A22, FUNCT_1:def 5;
then x in dom h by A1, A13, SETFAM_1:def 1;
then [z,x] in dom (uncurry f) by A23, FUNCT_5:def 4;
then A24: [x,z] in dom (uncurry' f) by A12, FUNCT_4:43;
[x,z] in [:(meet (doms f)),(dom f):] by A1, A13, A23, ZFMISC_1:106;
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:4;
then [x,z] in [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):] by A21, ZFMISC_1:106;
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:4; :: 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 13;
then reconsider h = f . z as Function by Def1;
A27: z in dom f by A10, A26, FUNCT_1:def 13;
then dom h = (doms f) . z by Th31;
then dom h in rng (doms f) by A2, A10, A26, FUNCT_1:def 5;
then A28: x in dom h by A1, A13, SETFAM_1:def 1;
then A29: h . x in rng h by FUNCT_1:def 5;
( 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:38;
then (uncurry' f) . (x,z) = g . z by FUNCT_1:70;
then g . z = h . x by A27, A28, FUNCT_5:46;
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;