theorem Th131: :: FINSEQ_3:133

for f, g being Function holds
( doms <*f,g*> = <*(dom f),(dom g)*> & rngs <*f,g*> = <*(rng f),(rng g)*> )