let f be Function; :: thesis: ( dom <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) )
A1: ( <:f:> = curry ((uncurry' f) | [:(meet (doms f)),(dom f):]) & dom (doms f) = f " (SubFuncs (rng f)) & dom (rngs f) = f " (SubFuncs (rng f)) ) by Def2, Def3;
dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) c= [:(meet (doms f)),(dom f):] by RELAT_1:87;
hence A2: 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) )
thus meet (doms f) c= dom <:f:> :: thesis: rng <:f:> c= product (rngs f)

proof

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;
consider y being Element of rng (doms f);
consider z being set such that
A5: ( z in dom (doms f) & y = (doms f) . z ) by A4, FUNCT_1:def 5;
A6: ( z in dom f & f . z in SubFuncs (rng f) ) by A1, A5, FUNCT_1:def 13;
then reconsider g = f . z as Function by Def1;
( y = dom g & x in y ) by A3, A4, A5, A6, Th31, SETFAM_1:def 1;
then ( [x,z] in dom (uncurry' f) & [x,z] in [:(meet (doms f)),(dom f):] ) by A3, A6, FUNCT_5:46, ZFMISC_1:106;
then [x,z] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by 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;

set f' = (uncurry' f) | [:(meet (doms f)),(dom f):];
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) )
assume y in rng <:f:> ; :: thesis: y in product (rngs f)
then consider x being set such that
A7: ( x in dom <:f:> & y = <:f:> . x ) by FUNCT_1:def 5;
reconsider g = y as Function by A7, FUNCT_5:37;
A8: ( dom g = proj2 ((dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) /\ [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):]) & dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) = (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] & ( for z being set st z in dom g holds
( g . z = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . x,z & [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) ) ) ) by A7, FUNCT_5:38, RELAT_1:90;
A9: uncurry' f = ~ (uncurry f) by FUNCT_5:def 6;
A10: 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 ( g . z = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . x,z & [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) ) by A7, FUNCT_5:38;
then [x,z] in dom (uncurry' f) by A8, XBOOLE_0:def 4;
then [z,x] in dom (uncurry f) by A9, FUNCT_4:43;
then consider y1 being set , h being Function, y2 being set such that
A11: ( [z,x] = [y1,y2] & y1 in dom f & h = f . y1 & y2 in dom h ) by FUNCT_5:def 4;
A12: ( z = y1 & x = y2 & h in rng f ) by A11, FUNCT_1:def 5, ZFMISC_1:33;
then f . z in SubFuncs (rng f) by A11, Def1;
hence z in dom (rngs f) by A1, A11, A12, 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 )
assume A13: z in dom (rngs f) ; :: thesis: z in dom g
then A14: ( z in dom (doms f) & z in dom f & f . z in SubFuncs (rng f) ) by A1, FUNCT_1:def 13;
then reconsider h = f . z as Function by Def1;
dom h = (doms f) . z by A14, Th31;
then dom h in rng (doms f) by A1, A13, FUNCT_1:def 5;
then x in dom h by A2, A7, SETFAM_1:def 1;
then [z,x] in dom (uncurry f) by A14, FUNCT_5:def 4;
then ( [x,z] in dom (uncurry' f) & [x,z] in [:(meet (doms f)),(dom f):] ) by A2, A7, A9, A14, FUNCT_4:43, ZFMISC_1:106;
then A15: [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A8, XBOOLE_0:def 4;
then ( z in proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) & x in {x} ) by FUNCT_5:4, TARSKI:def 1;
then [x,z] in [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):] by 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 A15, XBOOLE_0:def 4;
hence z in dom g by A8, 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 A16: z in dom (rngs f) ; :: thesis: g . z in (rngs f) . z
then A17: ( g . z = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . x,z & [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) & z in dom f & f . z in SubFuncs (rng f) & z in dom (doms f) ) by A1, A7, A10, FUNCT_1:def 13, FUNCT_5:38;
then reconsider h = f . z as Function by Def1;
dom h = (doms f) . z by A17, Th31;
then dom h in rng (doms f) by A1, A16, FUNCT_1:def 5;
then ( x in dom h & [x,z] in dom (uncurry' f) & (uncurry' f) . x,z = g . z ) by A2, A7, A8, A17, FUNCT_1:70, SETFAM_1:def 1, XBOOLE_0:def 4;
then ( g . z = h . x & h . x in rng h & (rngs f) . z = rng h ) by A17, Th31, FUNCT_1:def 5, FUNCT_5:46;
hence g . z in (rngs f) . z ; :: thesis: verum

end;

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

end;