let f, g be Function; ( 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 )
by FINSEQ_1:44;
A3:
( dom <*f,g*> = Seg 2 & {f,g} = {f,g} )
by FINSEQ_1:89;
A4:
( <*(rng f),(rng g)*> . 1 = rng f & <*(rng f),(rng g)*> . 2 = rng g )
by FINSEQ_1:44;
A5:
now for x being object st x in {1,2} holds
(rngs <*f,g*>) . x = <*(rng f),(rng g)*> . xlet x be
object ;
( x in {1,2} implies (rngs <*f,g*>) . x = <*(rng f),(rng g)*> . x )assume A6:
x in {1,2}
;
(rngs <*f,g*>) . x = <*(rng f),(rng g)*> . xthen
(
x = 1 or
x = 2 )
by TARSKI:def 2;
hence
(rngs <*f,g*>) . x = <*(rng f),(rng g)*> . x
by A2, A4, A3, A6, FINSEQ_1:2, FUNCT_6:def 3;
verum end;
A7:
( <*(dom f),(dom g)*> . 1 = dom f & <*(dom f),(dom g)*> . 2 = dom g )
by FINSEQ_1:44;
now for x being object st x in {1,2} holds
(doms <*f,g*>) . x = <*(dom f),(dom g)*> . xlet x be
object ;
( x in {1,2} implies (doms <*f,g*>) . x = <*(dom f),(dom g)*> . x )assume A8:
x in {1,2}
;
(doms <*f,g*>) . x = <*(dom f),(dom g)*> . xthen
(
x = 1 or
x = 2 )
by TARSKI:def 2;
hence
(doms <*f,g*>) . x = <*(dom f),(dom g)*> . x
by A2, A7, A3, A8, FINSEQ_1:2, FUNCT_6:def 2;
verum end;
hence
doms <*f,g*> = <*(dom f),(dom g)*>
by A1, A3, FINSEQ_1:2; 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; verum