theorem Th57: :: FUNCT_7:58

for f being Function
for p being FinSequence holds
( firstdom (<*f*> ^ p) = dom f & lastrng (p ^ <*f*>) = rng f )