theorem Th25: :: FUNCT_6:29

for f being Function-yielding Function holds
( dom <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) )