theorem Th60: :: FUNCT_7:61

for X being set
for p being FuncSequence st p <> {} holds
dom (compose (p,X)) = (firstdom p) /\ X