theorem :: FINSEQ_3:141

for h being Function holds
( dom <:<*h*>:> = dom h & ( for x being object st x in dom h holds
<:<*h*>:> . x = <*(h . x)*> ) )