dom (f ") = dom f by Def7;
hence f " is FinSequence-like by Lm1; :: thesis: verum