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