dom (r (#) f) = dom f by Def5;
hence r (#) f is FinSequence-like by Lm1; :: thesis: verum