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