theorem :: FINSEQ_6:158

for x being set
for f being FinSequence holds f ^' <*x*> = f