let h be Function; :: thesis: ( dom <:<*h*>:> = dom h & ( for x being set st x in dom h holds
<:<*h*>:> . x = <*(h . x)*> ) )
A1: 1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
A2: ( rng <:<*h*>:> c= product (rngs <*h*>) & rngs <*h*> = <*(rng h)*> ) by Th33, Th49;
thus A3: 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 A4: x in dom h ; :: thesis: <:<*h*>:> . x = <*(h . x)*>
then <:<*h*>:> . x in rng <:<*h*>:> by A3, FUNCT_1:def 5;
then consider g being Function such that
A5: <:<*h*>:> . x = g and
A6: dom g = dom <*(rng h)*> and
for y being set st y in dom <*(rng h)*> holds
g . y in <*(rng h)*> . y by A2, CARD_3:def 5;
A7: dom g = Seg 1 by A6, FINSEQ_1:55;
( dom <*h*> = Seg 1 & <*h*> . 1 = h ) by FINSEQ_1:55, FINSEQ_1:57;
then A8: (uncurry <*h*>) . (1,x) = h . x by A4, A1, FUNCT_5:45;
reconsider g = g as FinSequence by A7, FINSEQ_1:def 2;
A9: len g = 1 by A7, FINSEQ_1:def 3;
g . 1 = (uncurry <*h*>) . (1,x) by A3, A4, A5, A7, A1, Th51;
hence <:<*h*>:> . x = <*(h . x)*> by A5, A8, A9, FINSEQ_1:57; :: thesis: verum