theorem Th61: :: FUNCT_7:62
for p being FuncSequence holds dom (compose (p,(firstdom p))) = firstdom p