let f1, f2 be Function; ( dom <:<*f1,f2*>:> = (dom f1) /\ (dom f2) & ( for x being object st x in (dom f1) /\ (dom f2) holds
<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> ) )
A1:
dom <*f1,f2*> = Seg 2
by FINSEQ_1:89;
A2:
( rng <:<*f1,f2*>:> c= product (rngs <*f1,f2*>) & rngs <*f1,f2*> = <*(rng f1),(rng f2)*> )
by Th131, FUNCT_6:29;
thus A3: dom <:<*f1,f2*>:> =
meet (doms <*f1,f2*>)
by FUNCT_6:29
.=
meet <*(dom f1),(dom f2)*>
by Th131
.=
(dom f1) /\ (dom f2)
by Th134
; for x being object st x in (dom f1) /\ (dom f2) holds
<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*>
let x be object ; ( x in (dom f1) /\ (dom f2) implies <:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> )
assume A4:
x in (dom f1) /\ (dom f2)
; <:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*>
then
<:<*f1,f2*>:> . x in rng <:<*f1,f2*>:>
by A3, FUNCT_1:def 3;
then consider g being Function such that
A5:
<:<*f1,f2*>:> . x = g
and
A6:
dom g = dom <*(rng f1),(rng f2)*>
and
for y being object st y in dom <*(rng f1),(rng f2)*> holds
g . y in <*(rng f1),(rng f2)*> . y
by A2, CARD_3:def 5;
A7:
dom g = Seg 2
by A6, FINSEQ_1:89;
A8:
1 in Seg 2
by FINSEQ_1:2, TARSKI:def 2;
reconsider g = g as FinSequence by A7, FINSEQ_1:def 2;
A9:
2 in Seg 2
by FINSEQ_1:2, TARSKI:def 2;
then A10:
g . 2 = (uncurry <*f1,f2*>) . (2,x)
by A3, A4, A5, A7, FUNCT_6:31;
( <*f1,f2*> . 2 = f2 & x in dom f2 )
by A4, XBOOLE_0:def 4;
then A11:
(uncurry <*f1,f2*>) . (2,x) = f2 . x
by A1, A9, FUNCT_5:38;
A12:
len g = 2
by A7, FINSEQ_1:def 3;
( <*f1,f2*> . 1 = f1 & x in dom f1 )
by A4, XBOOLE_0:def 4;
then A13:
(uncurry <*f1,f2*>) . (1,x) = f1 . x
by A1, A8, FUNCT_5:38;
g . 1 = (uncurry <*f1,f2*>) . (1,x)
by A3, A4, A5, A7, A8, FUNCT_6:31;
hence
<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*>
by A5, A13, A10, A11, A12, FINSEQ_1:44; verum