theorem :: FUNCT_7:64

for p being FuncSequence
for f being Function st lastrng p c= dom f holds
p ^ <*f*> is FuncSequence