theorem :: FINSEQ_2:34

for x being set
for f being Function st x in dom f holds
f * <*x*> = <*(f . x)*>