dom (abs f) = dom f by Def11;
hence |.f.| is FinSequence-like by Lm1; :: thesis: verum