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

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

let x be object ; :: thesis: ( x in {1,2} implies (rngs <*f,g*>) . x = <*(rng f),(rng g)*> . x )
assume A6: 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 A2, A3, A6, FINSEQ_1:2, FUNCT_6:def 3; :: thesis: verum

end;

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

let x be object ; :: thesis: ( x in {1,2} implies (doms <*f,g*>) . x = <*(dom f),(dom g)*> . x )
assume A8: 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 A2, A3, A8, FINSEQ_1:2, FUNCT_6:def 2; :: thesis: verum

end;

hence doms <*f,g*> = <*(dom f),(dom g)*> by A1, A3, FINSEQ_1:2; :: thesis: rngs <*f,g*> = <*(rng f),(rng g)*>
( dom (rngs <*f,g*>) = dom <*f,g*> & dom <*(rng f),(rng g)*> = Seg 2 ) by FINSEQ_1:89, FUNCT_6:def 3;
hence rngs <*f,g*> = <*(rng f),(rng g)*> by A3, A5, FINSEQ_1:2; :: thesis: verum