theorem Th142: :: FINSEQ_3:144

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