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)*> )
A1: ( rng <*f,g,h*> = {f,g,h} & <*f,g,h*> " (rng <*f,g,h*>) = dom <*f,g,h*> ) by FINSEQ_2:148, RELAT_1:169;
A2: <*(rng f),(rng g),(rng h)*> . 3 = rng h by FINSEQ_1:62;
A3: ( <*f,g,h*> . 1 = f & <*f,g,h*> . 2 = g ) by FINSEQ_1:62;
A4: <*f,g,h*> . 3 = h by FINSEQ_1:62;
A5: ( dom <*f,g,h*> = Seg 3 & SubFuncs {f,g,h} = {f,g,h} ) by Th29, FINSEQ_3:30;
A6: ( <*(rng f),(rng g),(rng h)*> . 1 = rng f & <*(rng f),(rng g),(rng h)*> . 2 = rng g ) by FINSEQ_1:62;

A7: now

let x be set ; :: thesis: ( x in {1,2,3} implies (rngs <*f,g,h*>) . x = <*(rng f),(rng g),(rng h)*> . x )
assume A8: 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 A1, A3, A4, A6, A2, A5, A8, Def3, FINSEQ_3:1; :: thesis: verum

end;

A9: ( dom (doms <*f,g,h*>) = <*f,g,h*> " (SubFuncs (rng <*f,g,h*>)) & dom <*(dom f),(dom g),(dom h)*> = Seg 3 ) by Def2, FINSEQ_3:30;
A10: <*(dom f),(dom g),(dom h)*> . 3 = dom h by FINSEQ_1:62;
A11: ( <*(dom f),(dom g),(dom h)*> . 1 = dom f & <*(dom f),(dom g),(dom h)*> . 2 = dom g ) by FINSEQ_1:62;

now

let x be set ; :: thesis: ( x in {1,2,3} implies (doms <*f,g,h*>) . x = <*(dom f),(dom g),(dom h)*> . x )
assume A12: 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 A1, A3, A4, A11, A10, A5, A12, Def2, FINSEQ_3:1; :: thesis: verum

end;

hence doms <*f,g,h*> = <*(dom f),(dom g),(dom h)*> by A1, A9, A5, FINSEQ_3:1, FUNCT_1:9; :: thesis: rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*>
( dom (rngs <*f,g,h*>) = <*f,g,h*> " (SubFuncs (rng <*f,g,h*>)) & dom <*(rng f),(rng g),(rng h)*> = Seg 3 ) by Def3, FINSEQ_3:30;
hence rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*> by A1, A5, A7, FINSEQ_3:1, FUNCT_1:9; :: thesis: verum