theorem :: FUNCT_7:63

for p being FuncSequence
for f being Function st rng f c= firstdom p holds
<*f*> ^ p is FuncSequence