let f1, f2 be Function; :: thesis: ( dom <:<*f1,f2*>:> = (dom f1) /\ (dom f2) & ( for x being set st x in (dom f1) /\ (dom f2) holds
<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> ) )
thus A1: dom <:<*f1,f2*>:> = meet (doms <*f1,f2*>) by Th49
.= meet <*(dom f1),(dom f2)*> by Th34
.= (dom f1) /\ (dom f2) by Th40 ; :: thesis: for x being set st x in (dom f1) /\ (dom f2) holds
<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*>
let x be set ; :: thesis: ( x in (dom f1) /\ (dom f2) implies <:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> )
assume A2: x in (dom f1) /\ (dom f2) ; :: thesis: <:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*>
then ( <:<*f1,f2*>:> . x in rng <:<*f1,f2*>:> & rng <:<*f1,f2*>:> c= product (rngs <*f1,f2*>) ) by A1, Th49, FUNCT_1:def 5;
then ( <:<*f1,f2*>:> . x in product (rngs <*f1,f2*>) & rngs <*f1,f2*> = <*(rng f1),(rng f2)*> ) by Th34;
then consider g being Function such that
A3: ( <:<*f1,f2*>:> . x = g & dom g = dom <*(rng f1),(rng f2)*> & ( for y being set st y in dom <*(rng f1),(rng f2)*> holds
g . y in <*(rng f1),(rng f2)*> . y ) ) by CARD_3:def 5;
A4: ( dom g = Seg 2 & dom <*f1,f2*> = Seg 2 & 1 in Seg 2 & 2 in Seg 2 & <*f1,f2*> . 1 = f1 & <*f1,f2*> . 2 = f2 & x in dom f1 & x in dom f2 ) by A2, A3, FINSEQ_1:4, FINSEQ_1:61, FINSEQ_3:29, TARSKI:def 2, XBOOLE_0:def 4;
then reconsider g = g as FinSequence by FINSEQ_1:def 2;
( g . 1 = (uncurry <*f1,f2*>) . 1,x & (uncurry <*f1,f2*>) . 1,x = f1 . x & g . 2 = (uncurry <*f1,f2*>) . 2,x & (uncurry <*f1,f2*>) . 2,x = f2 . x & len g = 2 ) by A1, A2, A3, A4, Th51, FINSEQ_1:def 3, FUNCT_5:45;
hence <:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> by A3, FINSEQ_1:61; :: thesis: verum