theorem Th56: :: FUNCT_7:57

( firstdom {} = {} & lastrng {} = {} ) by Def5, Def6;