let h be Function; :: thesis: ( dom <:<*h*>:> = dom h & ( for x being object st x in dom h holds
<:<*h*>:> . x = <*(h . x)*> ) )
A1: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
A2: ( rng <:<*h*>:> c= product (rngs <*h*>) & rngs <*h*> = <*(rng h)*> ) by Th130, FUNCT_6:29;
thus A3: dom <:<*h*>:> = meet (doms <*h*>) by FUNCT_6:29
.= meet <*(dom h)*> by Th130
.= dom h by Th133 ; :: thesis: for x being object st x in dom h holds
<:<*h*>:> . x = <*(h . x)*>
let x be object ; :: 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 3;
then consider g being Function such that
A5: <:<*h*>:> . x = g and
A6: dom g = dom <*(rng h)*> and
for y being object 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:38;
( dom <*h*> = Seg 1 & <*h*> . 1 = h ) by FINSEQ_1:38, FINSEQ_1:40;
then A8: (uncurry <*h*>) . (1,x) = h . x by A4, A1, FUNCT_5:38;
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, FUNCT_6:31;
hence <:<*h*>:> . x = <*(h . x)*> by A5, A8, A9, FINSEQ_1:40; :: thesis: verum