theorem :: FINSEQ_3:143

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