let f, g be Function; :: thesis: ( doms <*f,g*> = <*(dom f),(dom g)*> & rngs <*f,g*> = <*(rng f),(rng g)*> )
A1: ( rng <*f,g*> = {f,g} & <*f,g*> " (rng <*f,g*>) = dom <*f,g*> ) by FINSEQ_2:147, RELAT_1:169;
A2: ( dom (doms <*f,g*>) = <*f,g*> " (SubFuncs (rng <*f,g*>)) & dom <*(dom f),(dom g)*> = Seg 2 ) by Def2, FINSEQ_3:29;
A3: ( <*f,g*> . 1 = f & <*f,g*> . 2 = g ) by FINSEQ_1:61;
A4: ( dom <*f,g*> = Seg 2 & SubFuncs {f,g} = {f,g} ) by Th29, FINSEQ_3:29;
A5: ( <*(rng f),(rng g)*> . 1 = rng f & <*(rng f),(rng g)*> . 2 = rng g ) by FINSEQ_1:61;

A6: now

let x be set ; :: thesis: ( x in {1,2} implies (rngs <*f,g*>) . x = <*(rng f),(rng g)*> . x )
assume A7: x in {1,2} ; :: thesis: (rngs <*f,g*>) . x = <*(rng f),(rng g)*> . x
then ( x = 1 or x = 2 ) by TARSKI:def 2;
hence (rngs <*f,g*>) . x = <*(rng f),(rng g)*> . x by A1, A3, A5, A4, A7, Def3, FINSEQ_1:4; :: thesis: verum

end;

A8: ( <*(dom f),(dom g)*> . 1 = dom f & <*(dom f),(dom g)*> . 2 = dom g ) by FINSEQ_1:61;

now

let x be set ; :: thesis: ( x in {1,2} implies (doms <*f,g*>) . x = <*(dom f),(dom g)*> . x )
assume A9: x in {1,2} ; :: thesis: (doms <*f,g*>) . x = <*(dom f),(dom g)*> . x
then ( x = 1 or x = 2 ) by TARSKI:def 2;
hence (doms <*f,g*>) . x = <*(dom f),(dom g)*> . x by A1, A3, A8, A4, A9, Def2, FINSEQ_1:4; :: thesis: verum

end;

hence doms <*f,g*> = <*(dom f),(dom g)*> by A1, A2, A4, FINSEQ_1:4, FUNCT_1:9; :: thesis: rngs <*f,g*> = <*(rng f),(rng g)*>
( dom (rngs <*f,g*>) = <*f,g*> " (SubFuncs (rng <*f,g*>)) & dom <*(rng f),(rng g)*> = Seg 2 ) by Def3, FINSEQ_3:29;
hence rngs <*f,g*> = <*(rng f),(rng g)*> by A1, A4, A6, FINSEQ_1:4, FUNCT_1:9; :: thesis: verum