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