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