theorem Th61: :: FUNCT_7:62

for p being FuncSequence holds dom (compose (p,(firstdom p))) = firstdom p