let f, g, h be Function; :: thesis: ( doms <*f,g,h*> = <*(dom f),(dom g),(dom h)*> & rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*> )
A2: ( <*f,g,h*> . 1 = f & <*f,g,h*> . 2 = g ) ;
A3: <*f,g,h*> . 3 = h ;
A4: ( dom <*f,g,h*> = Seg 3 & {f,g,h} = {f,g,h} ) by FINSEQ_1:89;

A6: now :: thesis: for x being object st x in {1,2,3} holds
(rngs <*f,g,h*>) . x = <*(rng f),(rng g),(rng h)*> . x

let x be object ; :: thesis: ( x in {1,2,3} implies (rngs <*f,g,h*>) . x = <*(rng f),(rng g),(rng h)*> . x )
assume A7: x in {1,2,3} ; :: thesis: (rngs <*f,g,h*>) . x = <*(rng f),(rng g),(rng h)*> . x
then ( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1;
hence (rngs <*f,g,h*>) . x = <*(rng f),(rng g),(rng h)*> . x by A2, A3, A4, A7, Th1, FUNCT_6:def 3; :: thesis: verum

end;

A8: ( dom (doms <*f,g,h*>) = dom <*f,g,h*> & dom <*(dom f),(dom g),(dom h)*> = Seg 3 ) by FINSEQ_1:89, FUNCT_6:def 2;

now :: thesis: for x being object st x in {1,2,3} holds
(doms <*f,g,h*>) . x = <*(dom f),(dom g),(dom h)*> . x

let x be object ; :: thesis: ( x in {1,2,3} implies (doms <*f,g,h*>) . x = <*(dom f),(dom g),(dom h)*> . x )
assume A11: x in {1,2,3} ; :: thesis: (doms <*f,g,h*>) . x = <*(dom f),(dom g),(dom h)*> . x
then ( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1;
hence (doms <*f,g,h*>) . x = <*(dom f),(dom g),(dom h)*> . x by A2, A3, A4, A11, Th1, FUNCT_6:def 2; :: thesis: verum

end;

hence doms <*f,g,h*> = <*(dom f),(dom g),(dom h)*> by A8, A4, Th1; :: thesis: rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*>
( dom (rngs <*f,g,h*>) = dom <*f,g,h*> & dom <*(rng f),(rng g),(rng h)*> = Seg 3 ) by FINSEQ_1:89, FUNCT_6:def 3;
hence rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*> by A4, A6, Th1; :: thesis: verum