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