theorem Th130: :: FINSEQ_3:132

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